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/Induct/Term.thy
changeset 11549 e7265e70fd7c
parent 11046 b5f5942781a0
child 11649 dfb59b9954a6 
--- a/src/HOL/Induct/Term.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Induct/Term.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -48,11 +48,11 @@
     (!!f ts. list_all P ts ==> P (App f ts))
   ==> P t"
 proof -
-  case antecedent
+  case rule_context
   have "P t \<and> list_all P ts"
     apply (induct t and ts rule: term.induct)
-       apply (rule antecedent)
-      apply (rule antecedent)
+       apply (rule rule_context)
+      apply (rule rule_context)
       apply assumption
      apply simp_all
     done
isabelle