--- a/src/HOL/IMP/Big_Step.thy Tue Oct 22 16:07:09 2013 +0200
+++ b/src/HOL/IMP/Big_Step.thy Wed Oct 23 09:58:30 2013 +0200
@@ -268,11 +268,9 @@
subsection "Execution is deterministic"
text {* This proof is automatic. *}
-text_raw{*\snip{BigStepDeterministic}{0}{1}{% *}
+
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
by (induction arbitrary: u rule: big_step.induct) blast+
-text_raw{*}%endsnip*}
-
text {*
This is the proof as you might present it in a lecture. The remaining
--- a/src/HOL/IMP/Small_Step.thy Tue Oct 22 16:07:09 2013 +0200
+++ b/src/HOL/IMP/Small_Step.thy Wed Oct 23 09:58:30 2013 +0200
@@ -4,7 +4,6 @@
subsection "The transition relation"
-text_raw{*\snip{SmallStepDef}{0}{2}{% *}
inductive
small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
where
@@ -18,7 +17,6 @@
While: "(WHILE b DO c,s) \<rightarrow>
(IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
-text_raw{*}%endsnip*}
abbreviation