isabelle: src/HOL/Nat.ML@450c9b682a92 (annotated)

2441 decc46a5cdb5 added nat_induct2 oheimb parents: 2268 diff changeset	1	(* Title: HOL/Nat.ML
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	3	Author: Tobias Nipkow
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	4	Copyright 1997 TU Muenchen
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	7	goal thy "min 0 n = 0";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	8	br min_leastL 1;
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	9	by(trans_tac 1);
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	10	qed "min_0L";
1301 42782316d510 Added various thms and tactics. nipkow parents: 1264 diff changeset	11
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	12	goal thy "min n 0 = 0";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	13	br min_leastR 1;
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	14	by(trans_tac 1);
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	15	qed "min_0R";
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	16
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	17	goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	18	by(split_tac [expand_if] 1);
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	19	by(Simp_tac 1);
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	20	qed "min_Suc_Suc";
1660 8cb42cd97579 * empty log message * oheimb parents: 1618 diff changeset	21
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	22	Addsimps [min_0L,min_0R,min_Suc_Suc];

author	nipkow
	Wed, 12 Feb 1997 18:53:59 +0100
changeset 2608	450c9b682a92
parent 2441	decc46a5cdb5
child 3023	01364e2f30ad
permissions	-rw-r--r--