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/Lambda/ListBeta.thy
changeset 11549 e7265e70fd7c
parent 11183 0476c6e07bca
child 11639 4213422388c4 
--- a/src/HOL/Lambda/ListBeta.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -76,7 +76,7 @@
   ==> R"
 proof -
   assume major: "r $$ rs -> s"
-  case antecedent
+  case rule_context
   show ?thesis
     apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
     apply (assumption | rule refl | erule prems exE conjE impE disjE)+
isabelle