# HG changeset patch
# User nipkow
# Date 1429697508 -7200
# Node ID 2cd31c81e0e7b43307052b0bb7e383b76f6a9e5e
# Parent  b11401808dac66549afe5ed9df431291350007f3
added simp rules for ==>

diff -r b11401808dac -r 2cd31c81e0e7 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Apr 19 21:26:50 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Apr 22 12:11:48 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
 
diff -r b11401808dac -r 2cd31c81e0e7 src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sun Apr 19 21:26:50 2015 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Apr 22 12:11:48 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;
diff -r b11401808dac -r 2cd31c81e0e7 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Apr 19 21:26:50 2015 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 22 12:11:48 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
diff -r b11401808dac -r 2cd31c81e0e7 src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Sun Apr 19 21:26:50 2015 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy	Wed Apr 22 12:11:48 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
diff -r b11401808dac -r 2cd31c81e0e7 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Sun Apr 19 21:26:50 2015 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Apr 22 12:11:48 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])