src/HOL/Library/Quotient.thy
changeset 23394 474ff28210c0
parent 23373 ead82c82da9e
child 25062 af5ef0d4d655
     1.1 --- a/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/Quotient.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4    assumes "!!X Y. f X Y == g (pick X) (pick Y)"
     1.5      and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
     1.6    shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
     1.7 -  using prems and TrueI
     1.8 +  using assms and TrueI
     1.9    by (rule quot_cond_function)
    1.10  
    1.11  theorem quot_function':