src/HOL/Nat.ML
changeset 3023 01364e2f30ad
parent 2608 450c9b682a92
child 4686 74a12e86b20b
     1.1 --- a/src/HOL/Nat.ML	Wed Apr 23 11:12:10 1997 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Apr 23 11:18:29 1997 +0200
     1.3 @@ -5,18 +5,18 @@
     1.4  *)
     1.5  
     1.6  goal thy "min 0 n = 0";
     1.7 -br min_leastL 1;
     1.8 -by(trans_tac 1);
     1.9 +by (rtac min_leastL 1);
    1.10 +by (trans_tac 1);
    1.11  qed "min_0L";
    1.12  
    1.13  goal thy "min n 0 = 0";
    1.14 -br min_leastR 1;
    1.15 -by(trans_tac 1);
    1.16 +by (rtac min_leastR 1);
    1.17 +by (trans_tac 1);
    1.18  qed "min_0R";
    1.19  
    1.20  goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    1.21 -by(split_tac [expand_if] 1);
    1.22 -by(Simp_tac 1);
    1.23 +by (split_tac [expand_if] 1);
    1.24 +by (Simp_tac 1);
    1.25  qed "min_Suc_Suc";
    1.26  
    1.27  Addsimps [min_0L,min_0R,min_Suc_Suc];