Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
936
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset 
     1
 
(*  Title: 	HOL/IMP/Hoare.thy
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset 
     2
 
    ID:
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset 
     3
 
    Author: 	Tobias Nipkow
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset 
     4
 
    Copyright   1995 TUM
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset 
     5
 












a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




     6


Semantic embedding of Hoare logic













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




     7


*)













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




     8














a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




     9


Hoare = Denotation +













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




    10


consts













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




    11


  spec:: "[state=>bool,com,state=>bool] => bool" ("{{(1_)}}/ (_)/ {{(1_)}}" 10)













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




    12


defs













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




    13


  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"













a6d7b4084761
Hoare logic



nipkow


parents: 

diff
changeset




    14


end















isabelle