# HG changeset patch
# User bauerg
# Date 974802705 -3600
# Node ID 2f33d0fd242e2c89b0c566d1046b38f026b1072c
# Parent  777d6bde7b47366ce8c49e9af940f8f2b5436618
alternative function definition;

diff -r 777d6bde7b47 -r 2f33d0fd242e src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Tue Nov 21 10:37:04 2000 +0100
+++ b/src/HOL/Library/Quotient.thy	Tue Nov 21 11:31:45 2000 +0100
@@ -206,4 +206,10 @@
   show ?thesis by (rule quot_cond_function)
 qed
 
+theorem quot_function':
+  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
+    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
+    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
+  by  (rule quot_function) (simp only: quot_equality)+
+
 end