--- a/Quot/quotient_tacs.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,10 @@
+(*  Title:      quotient_tacs.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Tactics for solving goal arising from lifting
+    theorems to quotient types.
+*)
+
 signature QUOTIENT_TACS =
 sig
   val regularize_tac: Proof.context -> int -> tactic