src/HOL/IMP/Hoare.thy
changeset 937 c7e599f524de
parent 936 a6d7b4084761
child 938 621be7ec81d7
equal deleted inserted replaced
936:a6d7b4084761 937:c7e599f524de
     1 (*  Title: 	HOL/IMP/Hoare.thy
     1 (*  Title: 	HOL/IMP/Hoare.thy
     2     ID:
     2     ID:         $$
     3     Author: 	Tobias Nipkow
     3     Author: 	Tobias Nipkow
     4     Copyright   1995 TUM
     4     Copyright   1995 TUM
     5 
     5 
     6 Semantic embedding of Hoare logic
     6 Semantic embedding of Hoare logic
     7 *)
     7 *)