changeset 1335 | 5e1c0540f285 |
child 1374 | 5e407f2a3323 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Examples.thy Fri Nov 17 09:04:10 1995 +0100 @@ -0,0 +1,20 @@ +(* Title: HOL/Hoare/Examples.thy + ID: $Id$ + Author: Norbert Galm + Copyright 1995 TUM + +Various arithmetic examples. +*) + +Examples = Hoare + Arith2 + + +syntax + "@1" :: "nat" ("1") + "@2" :: "nat" ("2") + +translations + "1" == "Suc(0)" + "2" == "Suc(Suc(0))" +end + +