--- a/src/HOL/Relation.thy Sat May 08 17:06:58 2010 -0700
+++ b/src/HOL/Relation.thy Sun May 09 09:39:01 2010 -0700
@@ -181,6 +181,12 @@
lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)"
by auto
+lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)"
+by auto
+
+lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)"
+by auto
+
subsection {* Reflexivity *}
--- a/src/HOL/Tools/Function/mutual.ML Sat May 08 17:06:58 2010 -0700
+++ b/src/HOL/Tools/Function/mutual.ML Sun May 09 09:39:01 2010 -0700
@@ -192,7 +192,7 @@
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
- THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
+ THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
|> restore_cond
|> export
end
--- a/src/HOL/Tools/Function/sum_tree.ML Sat May 08 17:06:58 2010 -0700
+++ b/src/HOL/Tools/Function/sum_tree.ML Sun May 09 09:39:01 2010 -0700
@@ -8,7 +8,6 @@
struct
(* Theory dependencies *)
-val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
val sumcase_split_ss =
HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})