src/HOL/Nat.ML
changeset 6433 228237ec56e5
parent 6301 08245f5a436d
child 6805 52b13dfbe954
     1.1 --- a/src/HOL/Nat.ML	Wed Apr 14 19:07:39 1999 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Apr 15 18:10:37 1999 +0200
     1.3 @@ -113,3 +113,17 @@
     1.4  qed "min_Suc_Suc";
     1.5  
     1.6  Addsimps [min_0L,min_0R,min_Suc_Suc];
     1.7 +
     1.8 +Goalw [max_def] "max 0 n = n";
     1.9 +by (Simp_tac 1);
    1.10 +qed "max_0L";
    1.11 +
    1.12 +Goalw [max_def] "max n 0 = n";
    1.13 +by (Simp_tac 1);
    1.14 +qed "max_0R";
    1.15 +
    1.16 +Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
    1.17 +by (Simp_tac 1);
    1.18 +qed "max_Suc_Suc";
    1.19 +
    1.20 +Addsimps [max_0L,max_0R,max_Suc_Suc];