changeset 1761 | 29e08d527ba1 |
parent 1760 | 6f41a494f3b1 |
child 2515 | 6ff9bd353121 |
--- a/src/HOL/subset.ML Thu May 23 14:37:06 1996 +0200 +++ b/src/HOL/subset.ML Thu May 23 15:15:20 1996 +0200 @@ -17,7 +17,7 @@ qed "subset_insert"; qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})" - (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]); + (fn _=> [ (Fast_tac 1) ]); (*** Big Union -- least upper bound of a set ***)