isabelle: src/HOL/Nat.thy@0c7e97836e3c (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Nat.thy
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: 2541 diff changeset	3	Author: Tobias Nipkow
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	4	Copyright 1997 TU Muenchen
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	6	Nat is a partial order
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	9	Nat = NatDef +
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	11	(*install 'automatic' induction tactic, pretending nat is a datatype
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	12	except for induct_tac and exhaust_tac, everything is dummy*)
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	13
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	14	MLtext {\|
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	15	\|> Dtype.add_datatype_info
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	16	("nat", {case_const = Bound 0, case_rewrites = [],
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	17	constructors = [], induct_tac = nat_ind_tac,
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	18	exhaustion = natE,
4613 67a726003cf8 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW nipkow parents: 4104 diff changeset	19	exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
67a726003cf8 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW nipkow parents: 4104 diff changeset	20	THEN_ALL_NEW (rotate_tac ~1),
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	21	nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	22	\|}
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	23
84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	24
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	25	instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	26
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	27	consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	28	"^" :: ['a::power,nat] => 'a (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	29
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	30	end

author	wenzelm
	Thu, 12 Feb 1998 17:53:05 +0100
changeset 4628	0c7e97836e3c
parent 4613	67a726003cf8
child 4640	ac6cf9f18653
permissions	-rw-r--r--