Mercurial Mercurial > repos > isabelle / 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.
src/HOL/Numeral.thy
changeset 11488 4ff900551340
parent 9410 612ee826a409
child 11699 c7df55158574 
--- a/src/HOL/Numeral.thy	Wed Aug 08 17:37:47 2001 +0200
+++ b/src/HOL/Numeral.thy	Wed Aug 08 17:38:29 2001 +0200
@@ -19,8 +19,13 @@
 consts
   number_of :: "bin => 'a::number"
 
+nonterminals
+  numeral
+
 syntax
-  "_Numeral" :: "xnum => 'a"    ("_")
+  "_constify" :: "xnum => numeral"    ("_")
+  "_Numeral" :: "numeral => 'a"    ("_")
+
 
 setup NumeralSyntax.setup
isabelle