# HG changeset patch
# User kleing
# Date 1320304247 -39600
# Node ID 4ef9220b886bfb26a03d43246757de27dba7aae0
# Parent  df7554ebe02471aa1a32eaab4ea046f610ed5001
more IMP fragments

diff -r df7554ebe024 -r 4ef9220b886b src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Thu Nov 03 18:10:13 2011 +1100
+++ b/src/HOL/IMP/Big_Step.thy	Thu Nov 03 18:10:47 2011 +1100
@@ -23,12 +23,14 @@
              (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]
 
@@ -228,7 +230,7 @@
   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)