Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Proofs/Lambda/NormalForm.thy
changeset 45605 a89b4bc311a5
parent 39157 b98909faaea8
child 58889 5b7a9633cfa8 
--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -132,10 +132,10 @@
   apply (drule listall_conj2)
   apply (drule_tac i=i and j=j in subst_terms_NF)
   apply assumption
-  apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])
+  apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
   apply simp
   apply (erule NF.App)
-  apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
+  apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
   apply simp
   apply (iprover intro: NF.App)
   apply simp
@@ -173,7 +173,7 @@
   apply (drule listall_conj2)
   apply (drule_tac i=i in lift_terms_NF)
   apply assumption
-  apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])
+  apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
   apply simp
   apply (rule NF.App)
   apply assumption
isabelle