equal
deleted
inserted
replaced
90 |
90 |
91 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
91 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
92 apply (induct m) |
92 apply (induct m) |
93 apply (case_tac n) |
93 apply (case_tac n) |
94 apply (case_tac [3] n) |
94 apply (case_tac [3] n) |
95 apply (simp del: simp_thms subst_all subst_all', iprover?)+ |
95 apply (simp del: simp_thms subst_all, iprover?)+ |
96 done |
96 done |
97 |
97 |
98 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" |
98 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" |
99 shows "listall NF ts" using NF |
99 shows "listall NF ts" using NF |
100 by cases simp_all |
100 by cases simp_all |