src/HOL/Hoare/Examples.thy
changeset 1625 40501958d0f6
parent 1476 608483c2122a
child 5646 7c2ddbaf8b8c
equal deleted inserted replaced
1624:e2a6102b9369 1625:40501958d0f6
     4     Copyright   1995 TUM
     4     Copyright   1995 TUM
     5 
     5 
     6 Various arithmetic examples.
     6 Various arithmetic examples.
     7 *)
     7 *)
     8 
     8 
     9 Examples = Hoare + Arith2 +
     9 Examples = Hoare + Arith2
    10 
       
    11 syntax
       
    12   "@1"  :: nat  ("1")
       
    13   "@2"  :: nat  ("2")
       
    14 
       
    15 translations
       
    16   "1" == "Suc(0)"
       
    17   "2" == "Suc(Suc(0))"
       
    18 end
       
    19 
       
    20