--- 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];
--- 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