# HG changeset patch
# User kleing
# Date 1312362552 -7200
# Node ID 376c1e7b320cf1cca12f3f0b6494a91380012407
# Parent  ee784502aed5c0186ec7b53919d660d7ac2a357a
fixed wrong isubs in IMP/Types

diff -r ee784502aed5 -r 376c1e7b320c src/HOL/IMP/Types.thy
--- 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! *)