src/HOL/subset.ML
changeset 7007 b46ccfee8e59
parent 5316 7a8975451a89
child 11603 c3724decadef
     1.1 --- a/src/HOL/subset.ML	Wed Jul 14 13:32:21 1999 +0200
     1.2 +++ b/src/HOL/subset.ML	Thu Jul 15 10:27:54 1999 +0200
     1.3 @@ -9,8 +9,10 @@
     1.4  
     1.5  (*** insert ***)
     1.6  
     1.7 -qed_goal "subset_insertI" Set.thy "B <= insert a B"
     1.8 - (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
     1.9 +Goal "B <= insert a B";
    1.10 +by (rtac subsetI 1);
    1.11 +by (etac insertI2 1) ;
    1.12 +qed "subset_insertI";
    1.13  
    1.14  Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
    1.15  by (Blast_tac 1);
    1.16 @@ -89,8 +91,9 @@
    1.17  
    1.18  (*** Set difference ***)
    1.19  
    1.20 -qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)"
    1.21 - (fn _ => [ (Blast_tac 1) ]);
    1.22 +Goal "A-B <= (A::'a set)";
    1.23 +by (Blast_tac 1) ;
    1.24 +qed "Diff_subset";
    1.25  
    1.26  (*** Monotonicity ***)
    1.27