src/HOL/IMP/Hoare.thy
changeset 936 a6d7b4084761
child 937 c7e599f524de
equal deleted inserted replaced
935:a94ef3eed456 936:a6d7b4084761
       
     1 (*  Title: 	HOL/IMP/Hoare.thy
       
     2     ID:
       
     3     Author: 	Tobias Nipkow
       
     4     Copyright   1995 TUM
       
     5 
       
     6 Semantic embedding of Hoare logic
       
     7 *)
       
     8 
       
     9 Hoare = Denotation +
       
    10 consts
       
    11   spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
       
    12 defs
       
    13   spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
       
    14 end