Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy
authorpaulson
Thu Mar 28 12:25:55 1996 +0100 (1996-03-28)
changeset 162540501958d0f6
parent 1624 e2a6102b9369
child 1626 12560b3ebf2c
Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy
src/HOL/Hoare/Examples.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Hoare/Examples.thy	Thu Mar 28 10:56:10 1996 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Thu Mar 28 12:25:55 1996 +0100
     1.3 @@ -6,15 +6,4 @@
     1.4  Various arithmetic examples.
     1.5  *)
     1.6  
     1.7 -Examples = Hoare + Arith2 +
     1.8 -
     1.9 -syntax
    1.10 -  "@1"  :: nat  ("1")
    1.11 -  "@2"  :: nat  ("2")
    1.12 -
    1.13 -translations
    1.14 -  "1" == "Suc(0)"
    1.15 -  "2" == "Suc(Suc(0))"
    1.16 -end
    1.17 -
    1.18 -
    1.19 +Examples = Hoare + Arith2
     2.1 --- a/src/HOL/Nat.thy	Thu Mar 28 10:56:10 1996 +0100
     2.2 +++ b/src/HOL/Nat.thy	Thu Mar 28 12:25:55 1996 +0100
     2.3 @@ -44,6 +44,8 @@
     2.4  
     2.5  consts
     2.6    "0"       :: nat                ("0")
     2.7 +  "1"       :: nat                ("1")
     2.8 +  "2"       :: nat                ("2")
     2.9    Suc       :: nat => nat
    2.10    nat_case  :: ['a, nat => 'a, nat] => 'a
    2.11    pred_nat  :: "(nat * nat) set"
    2.12 @@ -52,6 +54,8 @@
    2.13    Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    2.14  
    2.15  translations
    2.16 +   "1"  == "Suc(0)"
    2.17 +   "2"  == "Suc(1)"
    2.18    "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    2.19  
    2.20  defs