src/HOL/IMP/Hoare.thy
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"