--- 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
--- 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)