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_no_result;
authorwenzelm
Tue, 16 Oct 2001 17:52:07 +0200
changeset 11804 d69e7acd9380
parent 11803 30f2104953a1
child 11805 b110a1ea90da
TypedefPackage.add_typedef_no_result;
src/HOL/thy_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/thy_syntax.ML	Tue Oct 16 17:51:50 2001 +0200
+++ b/src/HOL/thy_syntax.ML	Tue Oct 16 17:52:07 2001 +0200
@@ -280,7 +280,7 @@
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|",
   "and", "distinct", "inject", "induct"]
- [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
+ [axm_section "typedef" "|> TypedefPackage.add_typedef_no_result" typedef_decl,
   section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
   section "inductive" 	"" (inductive_decl false),
   section "coinductive"	"" (inductive_decl true),
isabelle