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 23394 474ff28210c0
parent 23373 ead82c82da9e
child 25062 af5ef0d4d655 
--- a/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -185,7 +185,7 @@
   assumes "!!X Y. f X Y == g (pick X) (pick Y)"
     and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
-  using prems and TrueI
+  using assms and TrueI
   by (rule quot_cond_function)
 
 theorem quot_function':
isabelle