src/HOL/IMP/Big_Step.thy

--- a/src/HOL/IMP/Big_Step.thy	Fri Sep 07 07:20:55 2012 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Fri Sep 07 08:35:35 2012 +0200
@@ -4,7 +4,7 @@
 
 subsection "Big-Step Semantics of Commands"
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepdef}{% *}
+text_raw{*\snip{BigStepdef}{0}{1}{% *}
 inductive
   big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
 where
@@ -21,16 +21,16 @@
 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
 WhileTrue:  "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
              (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}
+text_raw{*\snip{BigStepEx}{1}{2}{% *}
 schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
 apply(rule Seq)
 apply(rule Assign)
 apply simp
 apply(rule Assign)
 done
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 thm ex[simplified]
 
@@ -130,11 +130,11 @@
   in @{text s'} iff @{text c'} started in the same @{text s} also terminates
   in the same @{text s'}}. Formally:
 *}
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEquiv}{% *}
+text_raw{*\snip{BigStepEquiv}{0}{1}{% *}
 abbreviation
   equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where
   "c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t  =  (c',s) \<Rightarrow> t)"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 text {*
 Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces).
@@ -220,17 +220,17 @@
 subsection "Execution is deterministic"
 
 text {* This proof is automatic. *}
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDeterministic}{% *}
+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{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 
 text {*
   This is the proof as you might present it in a lecture. The remaining
   cases are simple enough to be proved automatically:
 *}
-text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDetLong}{% *}
+text_raw{*\snip{BigStepDetLong}{0}{2}{% *}
 theorem
   "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
 proof (induction arbitrary: t' rule: big_step.induct)
@@ -250,6 +250,6 @@
   from c IHc have "s1' = s1" by blast
   with w IHw show "t' = t" by blast
 qed blast+ -- "prove the rest automatically"
-text_raw{*}\end{isaverbatimwrite}*}
+text_raw{*}%endsnip*}
 
 end