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/Library/Quotient.thy
changeset 11549 e7265e70fd7c
parent 11099 b301d1f72552
child 12338 de0f4a63baa5 
--- a/src/HOL/Library/Quotient.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Quotient.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -203,7 +203,7 @@
     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
 proof -
-  case antecedent from this TrueI
+  case rule_context from this TrueI
   show ?thesis by (rule quot_cond_function)
 qed
isabelle