moved "1", "2" to syntax section;
authorwenzelm
Wed Nov 27 16:45:57 1996 +0100 (1996-11-27)
changeset 22588ad8ee759d9f
parent 2257 c8154379738c
child 2259 e6d738f2b9a9
moved "1", "2" to syntax section;
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Wed Nov 27 16:42:48 1996 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Nov 27 16:45:57 1996 +0100
     1.3 @@ -44,8 +44,6 @@
     1.4  
     1.5  consts
     1.6    "0"       :: nat                ("0")
     1.7 -  "1"       :: nat                ("1")
     1.8 -  "2"       :: nat                ("2")
     1.9    Suc       :: nat => nat
    1.10    nat_case  :: ['a, nat => 'a, nat] => 'a
    1.11    pred_nat  :: "(nat * nat) set"
    1.12 @@ -53,6 +51,10 @@
    1.13  
    1.14    Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    1.15  
    1.16 +syntax
    1.17 +  "1"       :: nat                ("1")
    1.18 +  "2"       :: nat                ("2")
    1.19 +
    1.20  translations
    1.21     "1"  == "Suc(0)"
    1.22     "2"  == "Suc(1)"