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