src/HOL/Hoare/Examples.thy
changeset 1625 40501958d0f6
parent 1476 608483c2122a
child 5646 7c2ddbaf8b8c
     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