author nipkow Wed, 22 Apr 2015 12:15:27 +0200 changeset 60144 50eb4fdd5860 parent 60141 833adf7db7d8 (current diff) parent 60143 2cd31c81e0e7 (diff) child 60145 123ac30760df
merged
```--- a/src/HOL/Algebra/Divisibility.thy	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Apr 22 12:15:27 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	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Apr 22 12:15:27 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	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/HOL.thy	Wed Apr 22 12:15:27 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	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy	Wed Apr 22 12:15:27 2015 +0200
@@ -2865,13 +2865,7 @@
using ty_cases sum_cases
apply(drule_tac x="x" in meta_spec)
-apply(rotate_tac 10)
-apply(drule_tac x="a" in meta_spec)
-apply(rotate_tac 10)
-apply(drule_tac x="a" in meta_spec)
done

termination```
```--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Apr 21 17:19:00 2015 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Apr 22 12:15:27 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])```