--- /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
+
+