Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_typ.ML
changeset 766 df053507edba
parent 762 baac4639ecef
child 780 a24e26f5488c 
--- a/Quot/quotient_typ.ML	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/quotient_typ.ML	Sun Dec 20 00:26:53 2009 +0100
@@ -219,8 +219,8 @@
 val _ = OuterKeyword.keyword "/"
 
 val _ = 
-    OuterSyntax.local_theory_to_proof "quotient" 
-      "quotient type definitions (requires equivalence proofs)"
+    OuterSyntax.local_theory_to_proof "quotient_type" 
+      "quotient type definitions (require equivalence proofs)"
          OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)
nominal2