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 ***
nipkow@936
     1
(*  Title: 	HOL/IMP/Hoare.thy
nipkow@938
     2
    ID:         $Id$
nipkow@936
     3
    Author: 	Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
nipkow@936
     6
Semantic embedding of Hoare logic
nipkow@936
     7
*)
nipkow@936
     8
nipkow@936
     9
Hoare = Denotation +
nipkow@936
    10
consts
nipkow@936
    11
  spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
nipkow@936
    12
defs
nipkow@936
    13
  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
nipkow@936
    14
end