diff options
| author | Josh Chen | 2018-08-07 12:30:59 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-07 12:30:59 +0200 |
| commit | dc2730916482bd230f9bd5244b8b2cc9d005f69a (patch) | |
| tree | c551ba8af9d5f573367061a9e2a30eb962dcd54c /scratch.thy | |
| parent | fdecdc58f50bdc4527eb7c10e37651e5fd9690aa (diff) | |
Old application syntax incompatible with Eisbach
Diffstat (limited to '')
| -rw-r--r-- | scratch.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scratch.thy b/scratch.thy index b88a8fc..55e7023 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,9 +3,9 @@ theory scratch begin -abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)" +abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)" -schematic_goal "?a : (pred`0) =\<^sub>\<nat> 0" +schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0" apply (subst comp) apply (rule Nat_form) prefer 4 apply (subst comp) |