--- a/Quot/quotient_typ.ML Mon Jan 11 15:58:38 2010 +0100
+++ b/Quot/quotient_typ.ML Mon Jan 11 16:33:00 2010 +0100
@@ -39,9 +39,8 @@
end
-(********************************)
-(* definition of quotient types *)
-(********************************)
+
+(*** definition of quotient types ***)
val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
@@ -224,26 +223,27 @@
end
-(******************************)
-(* interface and syntax setup *)
-(******************************)
+
+(*** interface and syntax setup ***)
+
-(* the ML-interface takes a list of 5-tuples consisting of *)
-(* *)
-(* - the name of the quotient type *)
-(* - its free type variables (first argument) *)
-(* - its mixfix annotation *)
-(* - the type to be quotient *)
-(* - the relation according to which the type is quotient *)
-(* *)
-(* it opens a proof-state in which one has to show that the *)
-(* relations are equivalence relations *)
+(* the ML-interface takes a list of 5-tuples consisting of
+
+ - the name of the quotient type
+ - its free type variables (first argument)
+ - its mixfix annotation
+ - the type to be quotient
+ - the relation according to which the type is quotient
+
+ it opens a proof-state in which one has to show that the
+ relations are equivalence relations
+*)
fun quotient_type quot_list lthy =
let
(* sanity check *)
- val _ = map sanity_check quot_list
- val _ = map (map_check lthy) quot_list
+ val _ = List.app sanity_check quot_list
+ val _ = List.app (map_check lthy) quot_list
fun mk_goal (rty, rel) =
let