author | oheimb |
Fri, 01 May 1998 22:30:42 +0200 | |
changeset 4884 | 1ec740e30811 |
parent 4686 | 74a12e86b20b |
child 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
(* Title: HOL/Nat.ML ID: $Id$ Author: Tobias Nipkow Copyright 1997 TU Muenchen *) goal thy "min 0 n = 0"; by (rtac min_leastL 1); by (trans_tac 1); qed "min_0L"; goal thy "min n 0 = 0"; by (rtac min_leastR 1); by (trans_tac 1); qed "min_0R"; goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; by (Simp_tac 1); qed "min_Suc_Suc"; Addsimps [min_0L,min_0R,min_Suc_Suc];