# HG changeset patch
# User wenzelm
# Date 1002311399 -7200
# Node ID c7df5515857481e9899585af091632fb6fc666fb
# Parent  3b3feb92207a9e6d9cd13deac035422720219d05
"num" syntax;

diff -r 3b3feb92207a -r c7df55158574 src/HOL/Numeral.ML
--- a/src/HOL/Numeral.ML	Fri Oct 05 21:49:15 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/Numeral.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-*)
-
-(*Unfold all "let"s involving constants*)
-Goalw [Let_def] "Let (number_of v) f == f (number_of v)";
-by(Simp_tac 1);
-qed "Let_number_of";
-Addsimps [Let_number_of];
-
-(*The condition "True" is a hack to prevent looping.
-  Conditional rewrite rules are tried after unconditional ones, so a rule
-  like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
-Goal "True ==> (number_of w = x) = (x = number_of w)";
-by Auto_tac;  
-qed "number_of_reorient";
-Addsimps [number_of_reorient];
diff -r 3b3feb92207a -r c7df55158574 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Fri Oct 05 21:49:15 2001 +0200
+++ b/src/HOL/Numeral.thy	Fri Oct 05 21:49:59 2001 +0200
@@ -23,10 +23,27 @@
   numeral
 
 syntax
-  "_constify" :: "xnum => numeral"    ("_")
-  "_Numeral" :: "numeral => 'a"    ("_")
+  "_constify" :: "num => numeral"    ("_")
+  "_Numeral" :: "numeral => 'a"    ("#_")
+  Numeral0 :: 'a
+  Numeral1 :: 'a
+
+translations
+  "Numeral0" == "number_of Pls"
+  "Numeral1" == "number_of (Pls BIT True)"
 
 
 setup NumeralSyntax.setup
 
+
+(*Unfold all "let"s involving constants*)
+lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
+  by (simp add: Let_def)
+
+(*The condition "True" is a hack to prevent looping.
+  Conditional rewrite rules are tried after unconditional ones, so a rule
+  like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
+lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)"
+  by auto
+
 end