# HG changeset patch
# User haftmann
# Date 1329557745 -3600
# Node ID 42298c5d33b10f6041b0051cae347596c324af37
# Parent  69f45ffd5091a6c84b207dd622a5f56791153832
tuned proofs

diff -r 69f45ffd5091 -r 42298c5d33b1 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Sun Feb 12 22:10:05 2012 +0100
+++ b/src/HOL/ex/Primrec.thy	Sat Feb 18 10:35:45 2012 +0100
@@ -158,7 +158,7 @@
 
 lemma ack_add_bound2: "i < ack k j ==> i + j < ack (4 + k) j"
 apply (rule less_trans [of _ "ack k j + ack 0 j"])
- apply (blast intro: add_less_mono less_ack2) 
+ apply (blast intro: add_less_mono) 
 apply (rule ack_add_bound [THEN less_le_trans])
 apply simp
 done
diff -r 69f45ffd5091 -r 42298c5d33b1 src/HOL/ex/Set_Algebras.thy
--- a/src/HOL/ex/Set_Algebras.thy	Sun Feb 12 22:10:05 2012 +0100
+++ b/src/HOL/ex/Set_Algebras.thy	Sat Feb 18 10:35:45 2012 +0100
@@ -118,7 +118,7 @@
 
 theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
     a +o (C \<oplus> D)"
-  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
+  apply (auto intro!: simp add: elt_set_plus_def set_plus_def add_ac)
    apply (rule_tac x = "aa + ba" in exI)
    apply (auto simp add: add_ac)
   done
@@ -176,7 +176,7 @@
   by (auto simp add: elt_set_plus_def)
 
 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
-  apply (auto intro!: subsetI simp add: set_plus_def)
+  apply (auto intro!: simp add: set_plus_def)
   apply (rule_tac x = 0 in bexI)
    apply (rule_tac x = x in bexI)
     apply (auto simp add: add_ac)
@@ -229,7 +229,7 @@
 
 theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
     a *o (C \<otimes> D)"
-  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
+  apply (auto intro!: simp add: elt_set_times_def set_times_def
     mult_ac)
    apply (rule_tac x = "aa * ba" in exI)
    apply (auto simp add: mult_ac)
@@ -301,7 +301,7 @@
 
 lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
     a *o D \<oplus> C \<otimes> D"
-  apply (auto intro!: subsetI simp add:
+  apply (auto simp add:
     elt_set_plus_def elt_set_times_def set_times_def
     set_plus_def ring_distribs)
   apply auto