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_def.ML
changeset 767 37285ec4387d
parent 762 baac4639ecef
child 768 e9e205b904e2 
--- a/Quot/quotient_def.ML	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/quotient_def.ML	Sun Dec 20 00:53:35 2009 +0100
@@ -127,8 +127,9 @@
       (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
          OuterParse.term)
 
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
+val _ = OuterSyntax.local_theory "quotient_definition" 
+	  "definition for constants over the quotient type"
+             OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 
 end; (* structure *)
nominal2