# HG changeset patch
# User nipkow
# Date 1347881967 -7200
# Node ID 4ac2ed30edf3bb505bb3ea718af71e91d1b510fa
# Parent  a9d9f3483b7135233fad276775083fd166467a27
tuned

diff -r a9d9f3483b71 -r 4ac2ed30edf3 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Mon Sep 17 02:25:38 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Mon Sep 17 13:39:27 2012 +0200
@@ -172,7 +172,7 @@
 begin
 
 lemma mono_aval':
-  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
+  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
 by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
 
 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>