src/ZF/QUniv.ML
changeset 9211 6236c5285bd8
parent 6070 032babd0120b
child 9907 473a6604da94
     1.1 --- a/src/ZF/QUniv.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/QUniv.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      ZF/quniv
     1.5 +(*  Title:      ZF/QUniv
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -8,17 +8,14 @@
    1.10  
    1.11  (** Properties involving Transset and Sum **)
    1.12  
    1.13 -val [prem1,prem2] = goalw QUniv.thy [sum_def]
    1.14 -    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    1.15 -by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
    1.16 -by (REPEAT (etac (prem1 RS Transset_includes_range) 1
    1.17 -     ORELSE resolve_tac [conjI, singletonI] 1));
    1.18 +Goalw [sum_def] "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    1.19 +by (dtac (Un_subset_iff RS iffD1) 1);
    1.20 +by (blast_tac (claset() addDs [Transset_includes_range]) 1);
    1.21  qed "Transset_includes_summands";
    1.22  
    1.23 -val [prem] = goalw QUniv.thy [sum_def]
    1.24 -    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    1.25 +Goalw [sum_def] "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    1.26  by (stac Int_Un_distrib 1);
    1.27 -by (blast_tac (claset() addSDs [prem RS Transset_Pair_D]) 1);
    1.28 +by (blast_tac (claset() addDs [Transset_Pair_D]) 1);
    1.29  qed "Transset_sum_Int_subset";
    1.30  
    1.31  (** Introduction and elimination rules avoid tiresome folding/unfolding **)