--- a/src/HOL/IMP/VCG_Total_EX2.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/IMP/VCG_Total_EX2.thy Fri Jan 12 14:08:53 2018 +0100
@@ -12,8 +12,8 @@
with logical variables and proves soundness and completeness.
\<close>
-text{* Annotated commands: commands where loops are annotated with
-invariants. *}
+text\<open>Annotated commands: commands where loops are annotated with
+invariants.\<close>
datatype acom =
Askip ("SKIP") |
@@ -25,7 +25,7 @@
notation com.SKIP ("SKIP")
-text{* Strip annotations: *}
+text\<open>Strip annotations:\<close>
fun strip :: "acom \<Rightarrow> com" where
"strip SKIP = SKIP" |
@@ -34,7 +34,7 @@
"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |
"strip ({_/_} WHILE b DO C) = (WHILE b DO strip C)"
-text{* Weakest precondition from annotated commands: *}
+text\<open>Weakest precondition from annotated commands:\<close>
fun pre :: "acom \<Rightarrow> assn2 \<Rightarrow> assn2" where
"pre SKIP Q = Q" |
@@ -44,7 +44,7 @@
(\<lambda>l s. if bval b s then pre C\<^sub>1 Q l s else pre C\<^sub>2 Q l s)" |
"pre ({I/x} WHILE b DO C) Q = (\<lambda>l s. EX n. I (l(x:=n)) s)"
-text{* Verification condition: *}
+text\<open>Verification condition:\<close>
fun vc :: "acom \<Rightarrow> assn2 \<Rightarrow> bool" where
"vc SKIP Q = True" |
@@ -71,7 +71,7 @@
qed (auto intro: conseq Seq If simp: Skip Assign)
-text{* Completeness: *}
+text\<open>Completeness:\<close>
lemma pre_mono:
"\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> pre C P l s \<Longrightarrow> pre C P' l s"