changeset 45625 | 750c5a47400b |
parent 45607 | 16b4f5774621 |
child 45651 | 172aa230ce69 |
--- a/src/HOL/Set.thy Thu Nov 24 20:45:34 2011 +0100 +++ b/src/HOL/Set.thy Thu Nov 24 21:01:06 2011 +0100 @@ -369,7 +369,7 @@ *} declaration {* fn _ => - Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) + Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs)) *} lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"