moved "1", "2" to syntax section;
authorwenzelm
Wed, 27 Nov 1996 16:45:57 +0100
changeset 2258 8ad8ee759d9f
parent 2257 c8154379738c
child 2259 e6d738f2b9a9
moved "1", "2" to syntax section;
src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Nov 27 16:42:48 1996 +0100
+++ b/src/HOL/Nat.thy	Wed Nov 27 16:45:57 1996 +0100
@@ -44,8 +44,6 @@
 
 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"
@@ -53,6 +51,10 @@
 
   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
 
+syntax
+  "1"       :: nat                ("1")
+  "2"       :: nat                ("2")
+
 translations
    "1"  == "Suc(0)"
    "2"  == "Suc(1)"