src/HOL/IMP/Hoare.thy
author nipkow
Tue Mar 07 15:00:34 1995 +0100 (1995-03-07)
changeset 938 621be7ec81d7
parent 937 c7e599f524de
child 939 534955033ed2
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title: 	HOL/IMP/Hoare.thy
     2     ID:         $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