src/HOL/Ord.ML
changeset 2935 998cb95fdd43
parent 2608 450c9b682a92
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Ord.ML	Fri Apr 11 11:33:51 1997 +0200
     1.2 +++ b/src/HOL/Ord.ML	Fri Apr 11 15:21:36 1997 +0200
     1.3 @@ -25,26 +25,26 @@
     1.4  AddIffs [order_refl];
     1.5  
     1.6  goal Ord.thy "~ x < (x::'a::order)";
     1.7 -by(simp_tac (!simpset addsimps [order_less_le]) 1);
     1.8 +by (simp_tac (!simpset addsimps [order_less_le]) 1);
     1.9  qed "order_less_irrefl";
    1.10  AddIffs [order_less_irrefl];
    1.11  
    1.12  goal thy "(x::'a::order) <= y = (x < y | x = y)";
    1.13 -by(simp_tac (!simpset addsimps [order_less_le]) 1);
    1.14 -by(Fast_tac 1);
    1.15 +by (simp_tac (!simpset addsimps [order_less_le]) 1);
    1.16 +by (Blast_tac 1);
    1.17  qed "order_le_less";
    1.18  
    1.19  (** min **)
    1.20  
    1.21  goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
    1.22 -by(split_tac [expand_if] 1);
    1.23 -by(Asm_simp_tac 1);
    1.24 +by (split_tac [expand_if] 1);
    1.25 +by (Asm_simp_tac 1);
    1.26  qed "min_leastL";
    1.27  
    1.28  val prems = goalw thy [min_def]
    1.29   "(!!x::'a::order. least <= x) ==> min x least = least";
    1.30 -by(cut_facts_tac prems 1);
    1.31 -by(split_tac [expand_if] 1);
    1.32 -by(Asm_simp_tac 1);
    1.33 -by(fast_tac (!claset addEs [order_antisym]) 1);
    1.34 +by (cut_facts_tac prems 1);
    1.35 +by (split_tac [expand_if] 1);
    1.36 +by (Asm_simp_tac 1);
    1.37 +by (blast_tac (!claset addIs [order_antisym]) 1);
    1.38  qed "min_leastR";