# HG changeset patch
# User haftmann
# Date 1266826512 -3600
# Node ID 1cb90bbbf45e2f4175e88c5efd7aa2a9e789104d
# Parent  51692ec1b2201427869e4534b1cfde9ecd349eb2
tuned proofs

diff -r 51692ec1b220 -r 1cb90bbbf45e src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Mon Feb 22 09:15:11 2010 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Feb 22 09:15:12 2010 +0100
@@ -58,9 +58,8 @@
 apply (rule monoI)
 apply (unfold prefix_def)
 apply (erule genPrefix.induct, auto)
-apply (simp add: union_le_mono)
 apply (erule order_trans)
-apply (rule union_upper1)
+apply simp
 done
 
 (** setsum **)
diff -r 51692ec1b220 -r 1cb90bbbf45e src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Mon Feb 22 09:15:11 2010 +0100
+++ b/src/HOL/UNITY/Follows.thy	Mon Feb 22 09:15:12 2010 +0100
@@ -176,7 +176,7 @@
 apply (drule_tac x = "f xa" in spec)
 apply (drule_tac x = "g xa" in spec)
 apply (drule bspec, assumption) 
-apply (blast intro: union_le_mono order_trans)
+apply (blast intro: add_mono order_trans)
 done
 
 lemma Increasing_union: 
@@ -187,14 +187,14 @@
 apply (drule_tac x = "f xa" in spec)
 apply (drule_tac x = "g xa" in spec)
 apply (drule bspec, assumption) 
-apply (blast intro: union_le_mono order_trans)
+apply (blast intro: add_mono order_trans)
 done
 
 lemma Always_union:
      "[| F \<in> Always {s. f' s \<le> f s}; F \<in> Always {s. g' s \<le> g s} |]  
       ==> F \<in> Always {s. f' s + g' s \<le> f s + (g s :: ('a::order) multiset)}"
 apply (simp add: Always_eq_includes_reachable)
-apply (blast intro: union_le_mono)
+apply (blast intro: add_mono)
 done
 
 (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
@@ -211,7 +211,7 @@
 apply (rule PSP_Stable)
 apply (erule_tac x = "f s" in spec)
 apply (erule Stable_Int, assumption, blast)
-apply (blast intro: union_le_mono order_trans)
+apply (blast intro: add_mono order_trans)
 done
 
 (*The !! is there to influence to effect of permutative rewriting at the end*)