# HG changeset patch # User huffman # Date 1273423141 25200 # Node ID ba2a7096dd2bf414b938f690e48287533378465e # Parent 9e444b09fbef74992d1a5a661d0913832eb2a0b3# Parent acb789f3936bf1849abb9f0ba6a1d80e2a6a5d88 merged diff -r 9e444b09fbef -r ba2a7096dd2b src/HOL/Relation.thy --- 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 \ T) O R = (S O R) \ (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 *} diff -r 9e444b09fbef -r ba2a7096dd2b src/HOL/Tools/Function/mutual.ML --- 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 diff -r 9e444b09fbef -r ba2a7096dd2b src/HOL/Tools/Function/sum_tree.ML --- 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})