--- 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