src/HOL/Nat.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2608 450c9b682a92
child 3023 01364e2f30ad
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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 br min_leastL 1;
     9 by(trans_tac 1);
    10 qed "min_0L";
    11 
    12 goal thy "min n 0 = 0";
    13 br 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(split_tac [expand_if] 1);
    19 by(Simp_tac 1);
    20 qed "min_Suc_Suc";
    21 
    22 Addsimps [min_0L,min_0R,min_Suc_Suc];