changeset 68776 | 403dd13cf6e9 |
parent 67406 | 23307fd33906 |
--- a/src/HOL/IMP/Hoare.thy Fri Aug 17 11:26:35 2018 +0000 +++ b/src/HOL/IMP/Hoare.thy Mon Aug 20 20:54:26 2018 +0200 @@ -2,9 +2,9 @@ section "Hoare Logic" -theory Hoare imports Big_Step begin +subsection "Hoare Logic for Partial Correctness" -subsection "Hoare Logic for Partial Correctness" +theory Hoare imports Big_Step begin type_synonym assn = "state \<Rightarrow> bool"