changeset 1476 | 608483c2122a |
parent 1374 | 5e407f2a3323 |
child 1625 | 40501958d0f6 |
--- a/src/HOL/Hoare/Examples.thy Mon Feb 05 21:27:16 1996 +0100 +++ b/src/HOL/Hoare/Examples.thy Mon Feb 05 21:29:06 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Hoare/Examples.thy +(* Title: HOL/Hoare/Examples.thy ID: $Id$ - Author: Norbert Galm + Author: Norbert Galm Copyright 1995 TUM Various arithmetic examples. @@ -9,8 +9,8 @@ Examples = Hoare + Arith2 + syntax - "@1" :: nat ("1") - "@2" :: nat ("2") + "@1" :: nat ("1") + "@2" :: nat ("2") translations "1" == "Suc(0)"