Quot/quotient_typ.ML
changeset 952 9c3b3eaecaff
parent 918 7be9b054f672
child 1101 5eb84b817855
--- a/Quot/quotient_typ.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,10 @@
+(*  Title:      quotient_typ.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Definition of a quotient type.
+
+*)
+
 signature QUOTIENT_TYPE =
 sig
   val quotient_type: ((string list * binding * mixfix) * (typ * term)) list