--- a/src/HOL/Algebra/Divisibility.thy Wed Apr 22 12:43:06 2015 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Wed Apr 22 13:48:34 2015 +0200
@@ -2038,9 +2038,6 @@
using elems
unfolding Cs
apply (induct Cs', simp)
- apply clarsimp
- apply (subgoal_tac "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
- multiset_of (map (assocs G) cs) = multiset_of Cs'")
proof clarsimp
fix a Cs' cs
assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
@@ -2060,7 +2057,7 @@
show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
multiset_of (map (assocs G) cs) =
multiset_of Cs' + {#a#}" by fast
- qed simp
+ qed
thus ?thesis by (simp add: fmset_def)
qed
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Apr 22 12:43:06 2015 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Apr 22 13:48:34 2015 +0200
@@ -95,12 +95,12 @@
let
val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*)
val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
- val norm_eq_th =
+ val norm_eq_th = (* may collapse to True *)
simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
in
cut_tac norm_eq_th i
THEN (simp_tac cring_ctxt i)
- THEN (simp_tac cring_ctxt i)
+ THEN TRY(simp_tac cring_ctxt i)
end);
end;
--- a/src/HOL/HOL.thy Wed Apr 22 12:43:06 2015 +0100
+++ b/src/HOL/HOL.thy Wed Apr 22 13:48:34 2015 +0200
@@ -1292,7 +1292,8 @@
lemmas [simp] =
triv_forall_equality (*prunes params*)
- True_implies_equals (*prune asms `True'*)
+ True_implies_equals implies_True_equals (*prune True in asms*)
+ False_implies_equals (*prune False in asms*)
if_True
if_False
if_cancel
--- a/src/HOL/Nominal/Examples/Class2.thy Wed Apr 22 12:43:06 2015 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Wed Apr 22 13:48:34 2015 +0200
@@ -2865,13 +2865,7 @@
using ty_cases sum_cases
apply(auto simp add: ty.inject)
apply(drule_tac x="x" in meta_spec)
-apply(auto simp add: ty.inject)
-apply(rotate_tac 10)
-apply(drule_tac x="a" in meta_spec)
-apply(auto simp add: ty.inject)
-apply(rotate_tac 10)
-apply(drule_tac x="a" in meta_spec)
-apply(auto simp add: ty.inject)
+apply(fastforce simp add: ty.inject)
done
termination
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Apr 22 12:43:06 2015 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Apr 22 13:48:34 2015 +0200
@@ -173,7 +173,7 @@
next
assume neq: "x \<noteq> i"
from App have "listall ?R ts" by (iprover dest: listall_conj2)
- with TrueI TrueI uNF uT argsT
+ with uNF uT argsT
have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and>
NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
by (rule norm_list [of "\<lambda>t. t", simplified])