# HG changeset patch
# User kleing
# Date 1320810458 -39600
# Node ID bf39b07a7a8eec96bbddd83c0209d053e59b48ef
# Parent  8ca612982014c8519b5118ddb96c82204deb0a49
more fragments to export, removed the one from Com

diff -r 8ca612982014 -r bf39b07a7a8e src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Tue Nov 08 22:38:56 2011 +0100
+++ b/src/HOL/IMP/Com.thy	Wed Nov 09 14:47:38 2011 +1100
@@ -2,13 +2,11 @@
 
 theory Com imports BExp begin
 
-text_raw{*\begin{isaverbatimwrite}\newcommand{\Comdef}{% *}
 datatype
   com = SKIP 
       | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
       | Semi   com  com         ("_;/ _"  [60, 61] 60)
       | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
       | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
-text_raw{*}\end{isaverbatimwrite}*}
 
 end
diff -r 8ca612982014 -r bf39b07a7a8e src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Tue Nov 08 22:38:56 2011 +0100
+++ b/src/HOL/IMP/Small_Step.thy	Wed Nov 09 14:47:38 2011 +1100
@@ -4,6 +4,7 @@
 
 subsection "The transition relation"
 
+text_raw{*\begin{isaverbatimwrite}\newcommand{\SmallStepDef}{% *}
 inductive
   small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55)
 where
@@ -16,6 +17,7 @@
 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
 
 While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+text_raw{*}\end{isaverbatimwrite}*}
 
 
 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)