changeset 33102 | e3463e6db704 |
parent 32960 | 69916a850301 |
child 34943 | e97b22500a5c |
--- a/src/HOL/Library/Multiset.thy Sat Oct 24 20:47:10 2009 +0200 +++ b/src/HOL/Library/Multiset.thy Sun Oct 25 00:00:53 2009 +0200 @@ -1607,7 +1607,7 @@ rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single} val regroup_munion_conv = - FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus} + Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus} (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp})) fun unfold_pwleq_tac i =