src/HOL/Nat.ML
changeset 5069 3ea049f7979d
parent 4686 74a12e86b20b
child 5188 633ec5f6c155
     1.1 --- a/src/HOL/Nat.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -4,17 +4,17 @@
     1.4      Copyright   1997 TU Muenchen
     1.5  *)
     1.6  
     1.7 -goal thy "min 0 n = 0";
     1.8 +Goal "min 0 n = 0";
     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 +Goal "min n 0 = 0";
    1.15  by (rtac min_leastR 1);
    1.16  by (trans_tac 1);
    1.17  qed "min_0R";
    1.18  
    1.19 -goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    1.20 +Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    1.21  by (Simp_tac 1);
    1.22  qed "min_Suc_Suc";
    1.23