merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 17 Feb 2010 09:27:02 +0100
changeset 1167 e09d148ccc94
parent 1166 e860d8767d09 (diff)
parent 1165 f1253f280843 (current diff)
child 1168 5c1e16806901
merge
--- a/Quot/quotient_typ.ML	Wed Feb 17 09:26:38 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Feb 17 09:27:02 2010 +0100
@@ -302,8 +302,8 @@
 val _ = OuterKeyword.keyword "/"
 
 val _ =
-    OuterSyntax.local_theory_to_proof "quotient_type"
-      "quotient type definitions (require equivalence proofs)"
-         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+  OuterSyntax.local_theory_to_proof "quotient_type"
+    "quotient type definitions (require equivalence proofs)"
+       OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)