isabelle: src/HOL/Nat.ML@fc5773ae2790 (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";
3023 01364e2f30ad Ran expandshort paulson parents: 2608 diff changeset	8	by (rtac min_leastL 1);
01364e2f30ad Ran expandshort paulson parents: 2608 diff changeset	9	by (trans_tac 1);
2608 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";
3023 01364e2f30ad Ran expandshort paulson parents: 2608 diff changeset	13	by (rtac min_leastR 1);
01364e2f30ad Ran expandshort paulson parents: 2608 diff changeset	14	by (trans_tac 1);
2608 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)";
3023 01364e2f30ad Ran expandshort paulson parents: 2608 diff changeset	18	by (Simp_tac 1);
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	19	qed "min_Suc_Suc";
1660 8cb42cd97579 * empty log message * oheimb parents: 1618 diff changeset	20
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2441 diff changeset	21	Addsimps [min_0L,min_0R,min_Suc_Suc];

author	oheimb
	Mon, 27 Apr 1998 19:29:19 +0200
changeset 4836	fc5773ae2790
parent 4686	74a12e86b20b
child 5069	3ea049f7979d
permissions	-rw-r--r--