expandshort; tidied
authorpaulson
Tue Jul 27 10:30:26 1999 +0200 (1999-07-27)
changeset 7088a94c9e226c20
parent 7087 67c6706578ed
child 7089 9bfb8e218b99
expandshort; tidied
src/HOL/Univ.ML
     1.1 --- a/src/HOL/Univ.ML	Tue Jul 27 10:29:46 1999 +0200
     1.2 +++ b/src/HOL/Univ.ML	Tue Jul 27 10:30:26 1999 +0200
     1.3 @@ -404,38 +404,36 @@
     1.4  qed "Funs_mono";
     1.5  
     1.6  val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S";
     1.7 -br CollectI 1;
     1.8 -br subsetI 1;
     1.9 -be rangeE 1;
    1.10 -be ssubst 1;
    1.11 -br p 1;
    1.12 +by (rtac CollectI 1);
    1.13 +by (rtac subsetI 1);
    1.14 +by (etac rangeE 1);
    1.15 +by (etac ssubst 1);
    1.16 +by (rtac p 1);
    1.17  qed "FunsI";
    1.18  
    1.19  Goalw [Funs_def] "f : Funs S ==> f x : S";
    1.20 -be CollectE 1;
    1.21 -be subsetD 1;
    1.22 -br rangeI 1;
    1.23 +by (etac CollectE 1);
    1.24 +by (etac subsetD 1);
    1.25 +by (rtac rangeI 1);
    1.26  qed "FunsD";
    1.27  
    1.28  val [p1, p2] = goalw thy [o_def]
    1.29    "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
    1.30 -br ext 1;
    1.31 -br p2 1;
    1.32 -br (p1 RS FunsD) 1;
    1.33 +by (rtac (p2 RS ext) 1);
    1.34 +by (rtac (p1 RS FunsD) 1);
    1.35  qed "Funs_inv";
    1.36  
    1.37 -val [p1, p2] = Goalw [o_def] "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
    1.38 -by (cut_facts_tac [p1] 1);
    1.39 +val [p1, p2] = Goalw [o_def]
    1.40 +     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
    1.41  by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
    1.42 -br ext 1;
    1.43 -bd FunsD 1;
    1.44 -be rangeE 1;
    1.45 -be (exI RS (select_eq_Ex RS iffD2)) 1;
    1.46 +by (rtac ext 1);
    1.47 +by (rtac (p1 RS FunsD RS rangeE) 1);
    1.48 +by (etac (exI RS (select_eq_Ex RS iffD2)) 1);
    1.49  qed "Funs_rangeE";
    1.50  
    1.51  Goal "a : S ==> (%x. a) : Funs S";
    1.52  by (rtac FunsI 1);
    1.53 -by (atac 1);
    1.54 +by (assume_tac 1);
    1.55  qed "Funs_nonempty";
    1.56  
    1.57