src/HOL/Tools/Quotient/quotient_type.ML
changeset 47100 f8f788c8b7f3
parent 47096 3ea48c19673e
child 47308 9caab698dbe4
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:34:50 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Jan 16 12:33:26 2012 +0100
@@ -27,7 +27,7 @@
 val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
 val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
 
-(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
+(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
 fun typedef_term rel rty lthy =
   let
     val [x, c] =