| changeset 1552 | 6f71b5d46700 |
| parent 1531 | e5eb247ad13c |
| child 1631 | 26570790f089 |
--- a/src/HOL/subset.ML Wed Mar 06 12:19:16 1996 +0100 +++ b/src/HOL/subset.ML Wed Mar 06 12:52:11 1996 +0100 @@ -13,7 +13,7 @@ (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]); goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)"; -by(fast_tac set_cs 1); +by (fast_tac set_cs 1); qed "subset_insert"; (*** Big Union -- least upper bound of a set ***)