diff -r a94ef3eed456 -r a6d7b4084761 src/HOL/IMP/Hoare.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Hoare.thy	Tue Mar 07 14:57:37 1995 +0100
@@ -0,0 +1,14 @@
+(*  Title: 	HOL/IMP/Hoare.thy
+    ID:
+    Author: 	Tobias Nipkow
+    Copyright   1995 TUM
+
+Semantic embedding of Hoare logic
+*)
+
+Hoare = Denotation +
+consts
+  spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
+defs
+  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
+end