changeset 36773 | acb789f3936b |
parent 34232 | 36a2a3029fd3 |
child 37387 | 3581483cca6c |
--- a/src/HOL/Tools/Function/sum_tree.ML Sun May 09 12:00:43 2010 +0200 +++ b/src/HOL/Tools/Function/sum_tree.ML Sun May 09 15:28:44 2010 +0200 @@ -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})