src/HOL/IMP/Hoare.thy

--- a/src/HOL/IMP/Hoare.thy	Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/IMP/Hoare.thy	Thu Jun 06 14:39:44 1996 +0200
@@ -17,7 +17,7 @@
 syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
 translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
 
-inductive "hoare"
+inductive hoare
 intrs
   skip "|- {P}SKIP{P}"
   ass  "|- {%s.P(s[a s/x])} x:=a {P}"