src/HOL/Nat.ML
author nipkow
Sat Mar 07 16:29:29 1998 +0100 (1998-03-07)
changeset 4686 74a12e86b20b
parent 3023 01364e2f30ad
child 5069 3ea049f7979d
permissions -rw-r--r--
Removed `addsplits [expand_if]'
     1 (*  Title:      HOL/Nat.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TU Muenchen
     5 *)
     6 
     7 goal thy "min 0 n = 0";
     8 by (rtac min_leastL 1);
     9 by (trans_tac 1);
    10 qed "min_0L";
    11 
    12 goal thy "min n 0 = 0";
    13 by (rtac min_leastR 1);
    14 by (trans_tac 1);
    15 qed "min_0R";
    16 
    17 goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    18 by (Simp_tac 1);
    19 qed "min_Suc_Suc";
    20 
    21 Addsimps [min_0L,min_0R,min_Suc_Suc];