Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TypedefPackage.add_typedef;
authorwenzelm
Wed, 29 Apr 1998 11:44:30 +0200
changeset 4873 b5999638979e
parent 4872 33e7cdc20681
child 4874 c66a42846887
TypedefPackage.add_typedef; RecordPackage.add_record;
src/HOL/thy_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/thy_syntax.ML	Wed Apr 29 11:43:53 1998 +0200
+++ b/src/HOL/thy_syntax.ML	Wed Apr 29 11:44:30 1998 +0200
@@ -292,8 +292,8 @@
 
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
- [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
-  (section "record" "|> Record.add_record" record_decl),
+ [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
+  (section "record" "|> RecordPackage.add_record" record_decl),
   ("inductive", inductive_decl ""),
   ("coinductive", inductive_decl "Co"),
   (section "datatype" "" datatype_decl),
isabelle