# HG changeset patch
# User nipkow
# Date 1382515110 -7200
# Node ID a5eec4263b3ab2e62213c4e4cda1c61462818733
# Parent  7fba375a7e7d01ec5bd7d1e8123de01186cb7871
tuned

diff -r 7fba375a7e7d -r a5eec4263b3a src/HOL/IMP/Big_Step.thy
--- 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
diff -r 7fba375a7e7d -r a5eec4263b3a src/HOL/IMP/Small_Step.thy
--- 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