--- a/src/HOL/IMP/Types.thy Tue Aug 02 08:28:34 2011 -0700
+++ b/src/HOL/IMP/Types.thy Wed Aug 03 11:09:12 2011 +0200
@@ -17,7 +17,7 @@
"taval (V x) s (s x)" |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
\<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
-"taval a\<^isub>1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
+"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
\<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
inductive_cases [elim!]:
@@ -32,9 +32,9 @@
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (B bv) s bv" |
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
-"tbval b\<^isub>1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
-"taval a\<^isub>1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
-"taval a\<^isub>1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
+"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
+"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
+"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
subsection "Syntax of Commands"
(* a copy of Com.thy - keep in sync! *)