# HG changeset patch
# User wenzelm
# Date 1347888802 -7200
# Node ID caea18a5265fde8e1e8567623cf7ffb8f722b3ae
# Parent  4ac2ed30edf3bb505bb3ea718af71e91d1b510fa# Parent  617869cd779c8e377b8080fea288e07c136ceadd
merged

diff -r 617869cd779c -r caea18a5265f src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Mon Sep 17 15:32:16 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Mon Sep 17 15:33:22 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>