# HG changeset patch
# User paulson
# Date 828012355 -3600
# Node ID 40501958d0f644f8679c8f34d75d01f6521922b8
# Parent  e2a6102b9369f780411a7fc372ecc0e5a889b1a1
Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy

diff -r e2a6102b9369 -r 40501958d0f6 src/HOL/Hoare/Examples.thy
--- 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
diff -r e2a6102b9369 -r 40501958d0f6 src/HOL/Nat.thy
--- 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