isabelle: src/HOL/Nat.ML@548f398d770b (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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	7	Goal "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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	12	Goal "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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	17	Goalw [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	nipkow
	Tue, 23 Jun 1998 18:07:45 +0200
changeset 5071	548f398d770b
parent 5069	3ea049f7979d
child 5188	633ec5f6c155
permissions	-rw-r--r--