src/HOL/IMP/Hoare.thy
author nipkow
Tue Mar 07 14:59:24 1995 +0100 (1995-03-07)
changeset 937 c7e599f524de
parent 936 a6d7b4084761
child 938 621be7ec81d7
permissions -rw-r--r--
*** empty log message ***
     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