1
(* Title: HOL/Hoare/Examples.thy
2
ID: $Id$
3
Author: Norbert Galm
4
Copyright 1995 TUM
5
6
Various arithmetic examples.
7
*)
8
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