--- 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
--- 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