src/HOL/IMP/Hoare.thy
changeset 1789 aade046ec6d5
parent 1696 e84bff5c519b
child 2810 c4e16b36bc57
     1.1 --- a/src/HOL/IMP/Hoare.thy	Thu Jun 06 13:13:18 1996 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Thu Jun 06 14:39:44 1996 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
     1.5  translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
     1.6  
     1.7 -inductive "hoare"
     1.8 +inductive hoare
     1.9  intrs
    1.10    skip "|- {P}SKIP{P}"
    1.11    ass  "|- {%s.P(s[a s/x])} x:=a {P}"