src/HOL/IMP/Big_Step.thy

 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{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}
 schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
 apply(rule Semi)
 apply(rule Assign)
 apply simp
 apply(rule Assign)
 done
+text_raw{*}\end{isaverbatimwrite}*}
 
 thm ex[simplified]
 
 text{* We want to execute the big-step rules: *}
 

 
 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{\BigStepDet2}{% *}
+text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepDetLong}{% *}
 theorem
   "(c,s) \<Rightarrow> t  \<Longrightarrow>  (c,s) \<Rightarrow> t'  \<Longrightarrow>  t' = t"
 proof (induction arbitrary: t' rule: big_step.induct)
   -- "the only interesting case, @{text WhileTrue}:"
   fix b c s s1 t t'