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