# HG changeset patch
# User nipkow
# Date 1354894705 -3600
# Node ID eb7b59cc8e081424a3d91e65a61320d45c1079b3
# Parent  f1a27e82af16f33a58b3c577de985ce0fe56efa0
tuned text

diff -r f1a27e82af16 -r eb7b59cc8e08 src/HOL/IMP/HoareT.thy
--- a/src/HOL/IMP/HoareT.thy	Fri Dec 07 15:53:28 2012 +0100
+++ b/src/HOL/IMP/HoareT.thy	Fri Dec 07 16:38:25 2012 +0100
@@ -1,7 +1,9 @@
-header{* Hoare Logic for Total Correctness *}
+(* Author: Tobias Nipkow *)
 
 theory HoareT imports Hoare_Sound_Complete begin
 
+subsection "Hoare Logic for Total Correctness"
+
 text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
 works if execution is deterministic (which it is in our case). *}
 
diff -r f1a27e82af16 -r eb7b59cc8e08 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Fri Dec 07 15:53:28 2012 +0100
+++ b/src/HOL/IMP/VC.thy	Fri Dec 07 16:38:25 2012 +0100
@@ -1,8 +1,8 @@
-header "Verification Conditions"
+(* Author: Tobias Nipkow *)
 
 theory VC imports Hoare begin
 
-subsection "VCG via Weakest Preconditions"
+subsection "Verification Conditions"
 
 text{* Annotated commands: commands where loops are annotated with
 invariants. *}
@@ -46,7 +46,7 @@
 "strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
 "strip (Awhile I b c) = (WHILE b DO strip c)"
 
-subsection "Soundness"
+text {* Soundness: *}
 
 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}"
 proof(induction c arbitrary: Q)
@@ -68,7 +68,7 @@
 by (metis strengthen_pre vc_sound)
 
 
-subsection "Completeness"
+text{* Completeness: *}
 
 lemma pre_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
@@ -122,7 +122,7 @@
 qed
 
 
-subsection "An Optimization"
+text{* An Optimization: *}
 
 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
 "vcpre ASKIP Q = (\<lambda>s. True, Q)" |