--- a/src/HOL/Hoare/Examples.thy Thu Mar 28 10:56:10 1996 +0100
+++ b/src/HOL/Hoare/Examples.thy Thu Mar 28 12:25:55 1996 +0100
@@ -6,15 +6,4 @@
Various arithmetic examples.
*)
-Examples = Hoare + Arith2 +
-
-syntax
- "@1" :: nat ("1")
- "@2" :: nat ("2")
-
-translations
- "1" == "Suc(0)"
- "2" == "Suc(Suc(0))"
-end
-
-
+Examples = Hoare + Arith2
--- a/src/HOL/Nat.thy Thu Mar 28 10:56:10 1996 +0100
+++ b/src/HOL/Nat.thy Thu Mar 28 12:25:55 1996 +0100
@@ -44,6 +44,8 @@
consts
"0" :: nat ("0")
+ "1" :: nat ("1")
+ "2" :: nat ("2")
Suc :: nat => nat
nat_case :: ['a, nat => 'a, nat] => 'a
pred_nat :: "(nat * nat) set"
@@ -52,6 +54,8 @@
Least :: (nat=>bool) => nat (binder "LEAST " 10)
translations
+ "1" == "Suc(0)"
+ "2" == "Suc(1)"
"case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
defs