src/HOL/Nat.ML

moved inj and surj from Set to Fun and Inv -> inv.

(*  Title:      HOL/Nat.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1997 TU Muenchen
*)

goal thy "min 0 n = 0";
br min_leastL 1;
by(trans_tac 1);
qed "min_0L";

goal thy "min n 0 = 0";
br min_leastR 1;
by(trans_tac 1);
qed "min_0R";

goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
by(split_tac [expand_if] 1);
by(Simp_tac 1);
qed "min_Suc_Suc";

Addsimps [min_0L,min_0R,min_Suc_Suc];