# HG changeset patch
# User kuncar
# Date 1322675446 -3600
# Node ID fd8e140ae87980ec8188a4d9f03077c85c59a0a9
# Parent  3b7c35a08723890b7c5ceff46f6ed5ac66388bac
removed outdated comment moved back and updated (at the direct request of Christian Urban)

diff -r 3b7c35a08723 -r fd8e140ae879 src/HOL/Tools/Quotient/quotient_type.ML
--- 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 *)