New directory.
Hoare logic according to Mike Gordon.
(* 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