src/HOL/IMP/Hoare_Op.thy
changeset 41589 bbd861837ebc
parent 35754 8e7dba5f00f5
equal deleted inserted replaced
41588:9546828c0eb3 41589:bbd861837ebc
     1 (*  Title:      HOL/IMP/Hoare_Op.thy
     1 (*  Title:      HOL/IMP/Hoare_Op.thy
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow
     2     Author:     Tobias Nipkow
     4 *)
     3 *)
     5 
     4 
     6 header "Soundness and Completeness wrt Operational Semantics"
     5 header "Soundness and Completeness wrt Operational Semantics"
     7 
     6