Quot/quotient_def.ML
changeset 952 9c3b3eaecaff
parent 884 e49c6b6f37f4
child 1097 551eacf071d7
--- a/Quot/quotient_def.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,9 @@
+(*  Title:      quotient_def.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Definitions for constants on quotient types.
+
+*)
 
 signature QUOTIENT_DEF =
 sig