alternative function definition;
authorbauerg
Tue Nov 21 11:31:45 2000 +0100 (2000-11-21)
changeset 104992f33d0fd242e
parent 10498 777d6bde7b47
child 10500 df47f58b8253
alternative function definition;
src/HOL/Library/Quotient.thy
     1.1 --- a/src/HOL/Library/Quotient.thy	Tue Nov 21 10:37:04 2000 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Tue Nov 21 11:31:45 2000 +0100
     1.3 @@ -206,4 +206,10 @@
     1.4    show ?thesis by (rule quot_cond_function)
     1.5  qed
     1.6  
     1.7 +theorem quot_function':
     1.8 +  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
     1.9 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
    1.10 +    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.11 +  by  (rule quot_function) (simp only: quot_equality)+
    1.12 +
    1.13  end