--- a/src/HOL/Tools/Quotient/quotient_type.ML Wed Nov 30 15:07:10 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed Nov 30 18:50:46 2011 +0100
@@ -216,6 +216,20 @@
(*** interface and syntax setup ***)
+(* the ML-interface takes a list of tuples consisting of:
+
+ - the name of the quotient type
+ - its free type variables (first argument)
+ - its mixfix annotation
+ - the type to be quotient
+ - the partial flag (a boolean)
+ - the relation according to which the type is quotient
+ - optional names of morphisms (rep/abs)
+
+ 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 *)