src/HOL/IMP/Hoare.thy
author nipkow
Tue, 07 Mar 1995 14:57:37 +0100
changeset 936 a6d7b4084761
child 937 c7e599f524de
permissions -rw-r--r--
Hoare logic

(*  Title: 	HOL/IMP/Hoare.thy
    ID:
    Author: 	Tobias Nipkow
    Copyright   1995 TUM

Semantic embedding of Hoare logic
*)

Hoare = Denotation +
consts
  spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
defs
  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
end