src/HOL/Univ.ML
changeset 1761 29e08d527ba1
parent 1760 6f41a494f3b1
child 1786 8a31d85d27b8
     1.1 --- a/src/HOL/Univ.ML	Thu May 23 14:37:06 1996 +0200
     1.2 +++ b/src/HOL/Univ.ML	Thu May 23 15:15:20 1996 +0200
     1.3 @@ -430,15 +430,15 @@
     1.4  (**** UN x. B(x) rules ****)
     1.5  
     1.6  goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
     1.7 -by (fast_tac (!claset addIs [equalityI]) 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "ntrunc_UN1";
    1.10  
    1.11  goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
    1.12 -by (fast_tac (!claset addIs [equalityI]) 1);
    1.13 +by (Fast_tac 1);
    1.14  qed "Scons_UN1_x";
    1.15  
    1.16  goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
    1.17 -by (fast_tac (!claset addIs [equalityI]) 1);
    1.18 +by (Fast_tac 1);
    1.19  qed "Scons_UN1_y";
    1.20  
    1.21  goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
    1.22 @@ -556,16 +556,16 @@
    1.23  (*** Domain ***)
    1.24  
    1.25  goal Univ.thy "fst `` diag(A) = A";
    1.26 -by (fast_tac (!claset addIs [equalityI, diagI] addSEs [diagE]) 1);
    1.27 +by (fast_tac (!claset addIs [diagI] addSEs [diagE]) 1);
    1.28  qed "fst_image_diag";
    1.29  
    1.30  goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
    1.31 -by (fast_tac (!claset addIs [equalityI, uprodI, dprodI]
    1.32 +by (fast_tac (!claset addIs [uprodI, dprodI]
    1.33                       addSEs [uprodE, dprodE]) 1);
    1.34  qed "fst_image_dprod";
    1.35  
    1.36  goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
    1.37 -by (fast_tac (!claset addIs [equalityI, usum_In0I, usum_In1I, 
    1.38 +by (fast_tac (!claset addIs [usum_In0I, usum_In1I, 
    1.39                               dsum_In0I, dsum_In1I]
    1.40                       addSEs [usumE, dsumE]) 1);
    1.41  qed "fst_image_dsum";