src/HOL/Nat.ML
author wenzelm
Mon Jun 22 17:26:46 1998 +0200 (1998-06-22)
changeset 5069 3ea049f7979d
parent 4686 74a12e86b20b
child 5188 633ec5f6c155
permissions -rw-r--r--
isatool fixgoal;
oheimb@2441
     1
(*  Title:      HOL/Nat.ML
clasohm@923
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow
nipkow@2608
     4
    Copyright   1997 TU Muenchen
clasohm@923
     5
*)
clasohm@923
     6
wenzelm@5069
     7
Goal "min 0 n = 0";
paulson@3023
     8
by (rtac min_leastL 1);
paulson@3023
     9
by (trans_tac 1);
nipkow@2608
    10
qed "min_0L";
nipkow@1301
    11
wenzelm@5069
    12
Goal "min n 0 = 0";
paulson@3023
    13
by (rtac min_leastR 1);
paulson@3023
    14
by (trans_tac 1);
nipkow@2608
    15
qed "min_0R";
clasohm@923
    16
wenzelm@5069
    17
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
paulson@3023
    18
by (Simp_tac 1);
nipkow@2608
    19
qed "min_Suc_Suc";
oheimb@1660
    20
nipkow@2608
    21
Addsimps [min_0L,min_0R,min_Suc_Suc];