src/HOL/Hoare/Examples.thy
changeset 1476 608483c2122a
parent 1374 5e407f2a3323
child 1625 40501958d0f6
     1.1 --- a/src/HOL/Hoare/Examples.thy	Mon Feb 05 21:27:16 1996 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Mon Feb 05 21:29:06 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/Hoare/Examples.thy
     1.5 +(*  Title:      HOL/Hoare/Examples.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Norbert Galm
     1.8 +    Author:     Norbert Galm
     1.9      Copyright   1995 TUM
    1.10  
    1.11  Various arithmetic examples.
    1.12 @@ -9,8 +9,8 @@
    1.13  Examples = Hoare + Arith2 +
    1.14  
    1.15  syntax
    1.16 -  "@1"	:: nat	("1")
    1.17 -  "@2"	:: nat	("2")
    1.18 +  "@1"  :: nat  ("1")
    1.19 +  "@2"  :: nat  ("2")
    1.20  
    1.21  translations
    1.22    "1" == "Suc(0)"