isabelle: src/HOL/Hyperreal/CHANGES@6e5815f4d770 (annotated)

17334 6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	1	-- Changes from Isabelle 2004 version of HOL-Complex
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	2
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	3	* There is a new type constructor "star" for making nonstandard types.
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	4	The old type names are now type synonyms:
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	5	- hypreal = real star
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	6	- hypnat = nat star
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	7	- hcomplex = complex star
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	8
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	9	* Many groups of similarly-defined constants have been replaced by polymorphic
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	10	versions:
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	11
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	12	star_of <-- hypreal_of_real, hypnat_of_nat, hcomplex_of_complex
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	13
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	14	starset <-- starsetNat, starsetC
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	15	s <-- sNat, sc
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	16	starset_n <-- starsetNat_n, starsetC_n
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	17	sn <-- sNatn, scn
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	18	InternalSets <-- InternalNatSets, InternalCSets
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	19
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	20	starfun <-- starfunNat, starfunNat2, starfunC, starfunRC, starfunCR
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	21	f <-- fNat, fNat2, fc, fRc, fcR
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	22	starfun_n <-- starfunNat_n, starfunNat2_n, starfunC_n, starfunRC_n, starfunCR_n
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	23	fn <-- fNatn, fNat2n, fcn, fRcn, fcRn
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	24	InternalFuns <-- InternalNatFuns, InternalNatFuns2, InternalCFuns, InternalRCFuns, InternalCRFuns
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	25
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	26	* Many type-specific theorems have been removed in favor of theorems specific
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	27	to various axiomatic type classes:
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	28
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	29	add_commute <-- hypreal_add_commute, hypnat_add_commute, hcomplex_add_commute
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	30	add_assoc <-- hypreal_add_assoc, hypnat_add_assoc, hcomplex_add_assoc
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	31	OrderedGroup.add_0 <-- hypreal_add_zero_left, hypnat_add_zero_left, hcomplex_add_zero_left
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	32	OrderedGroup.add_0_right <-- hypreal_add_zero_right, hcomplex_add_zero_right
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	33	right_minus <-- hypreal_add_minus
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	34	left_minus <-- hypreal_add_minus_left, hcomplex_add_minus_left
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	35	mult_commute <-- hypreal_mult_commute, hypnat_mult_commute, hcomplex_mult_commute
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	36	mult_assoc <-- hypreal_mult_assoc, hypnat_mult_assoc, hcomplex_mult_assoc
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	37	mult_1_left <-- hypreal_mult_1, hypnat_mult_1, hcomplex_mult_one_left
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	38	mult_1_right <-- hcomplex_mult_one_right
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	39	mult_zero_left <-- hcomplex_mult_zero_left
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	40	left_distrib <-- hypreal_add_mult_distrib, hypnat_add_mult_distrib, hcomplex_add_mult_distrib
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	41	right_distrib <-- hypnat_add_mult_distrib2
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	42	zero_neq_one <-- hypreal_zero_not_eq_one, hypnat_zero_not_eq_one, hcomplex_zero_not_eq_one
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	43	right_inverse <-- hypreal_mult_inverse
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	44	left_inverse <-- hypreal_mult_inverse_left, hcomplex_mult_inv_left
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	45	order_refl <-- hypreal_le_refl, hypnat_le_refl
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	46	order_trans <-- hypreal_le_trans, hypnat_le_trans
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	47	order_antisym <-- hypreal_le_anti_sym, hypnat_le_anti_sym
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	48	order_less_le <-- hypreal_less_le, hypnat_less_le
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	49	linorder_linear <-- hypreal_le_linear, hypnat_le_linear
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	50	add_left_mono <-- hypreal_add_left_mono, hypnat_add_left_mono
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	51	mult_strict_left_mono <-- hypreal_mult_less_mono2, hypnat_mult_less_mono2
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	52	add_nonneg_nonneg <-- hypreal_le_add_order
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	53
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	54	* Separate theorems having to do with type-specific versions of constants have
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	55	been merged into theorems that apply to the new polymorphic constants:
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	56
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	57	STAR_UNIV_set <-- STAR_real_set, NatStar_real_set, STARC_complex_set
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	58	STAR_empty_set <-- NatStar_empty_set, STARC_empty_set
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	59	STAR_Un <-- NatStar_Un, STARC_Un
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	60	STAR_Int <-- NatStar_Int, STARC_Int
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	61	STAR_Compl <-- NatStar_Compl, STARC_Compl
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	62	STAR_subset <-- NatStar_subset, STARC_subset
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	63	STAR_mem <-- NatStar_mem, STARC_mem
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	64	STAR_mem_Compl <-- STARC_mem_Compl
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	65	STAR_diff <-- STARC_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	66	STAR_star_of_image_subset <-- STAR_hypreal_of_real_image_subset, NatStar_hypreal_of_real_image_subset, STARC_hcomplex_of_complex_image_subset
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	67	starset_n_Un <-- starsetNat_n_Un, starsetC_n_Un
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	68	starset_n_Int <-- starsetNat_n_Int, starsetC_n_Int
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	69	starset_n_Compl <-- starsetNat_n_Compl, starsetC_n_Compl
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	70	starset_n_diff <-- starsetNat_n_diff, starsetC_n_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	71	InternalSets_Un <-- InternalNatSets_Un, InternalCSets_Un
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	72	InternalSets_Int <-- InternalNatSets_Int, InternalCSets_Int
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	73	InternalSets_Compl <-- InternalNatSets_Compl, InternalCSets_Compl
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	74	InternalSets_diff <-- InternalNatSets_diff, InternalCSets_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	75	InternalSets_UNIV_diff <-- InternalNatSets_UNIV_diff, InternalCSets_UNIV_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	76	InternalSets_starset_n <-- InternalNatSets_starsetNat_n, InternalCSets_starsetC_n
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	77	starset_starset_n_eq <-- starsetNat_starsetNat_n_eq, starsetC_starsetC_n_eq
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	78	starset_n_starset <-- starsetNat_n_starsetNat, starsetC_n_starsetC
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	79	starfun_n_starfun <-- starfunNat_n_starfunNat, starfunNat2_n_starfunNat2, starfunC_n_starfunC, starfunRC_n_starfunRC, starfunCR_n_starfunCR
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	80	starfun <-- starfunNat, starfunNat2, starfunC, starfunRC, starfunCR
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	81	starfun_mult <-- starfunNat_mult, starfunNat2_mult, starfunC_mult, starfunRC_mult, starfunCR_mult
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	82	starfun_add <-- starfunNat_add, starfunNat2_add, starfunC_add, starfunRC_add, starfunCR_add
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	83	starfun_minus <-- starfunNat_minus, starfunNat2_minus, starfunC_minus, starfunRC_minus, starfunCR_minus
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	84	starfun_diff <-- starfunC_diff, starfunRC_diff, starfunCR_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	85	starfun_o <-- starfunNatNat2_o, starfunNat2_o, starfun_stafunNat_o, starfunC_o, starfunC_starfunRC_o, starfun_starfunCR_o
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	86	starfun_o2 <-- starfunNatNat2_o2, starfun_stafunNat_o2, starfunC_o2, starfunC_starfunRC_o2, starfun_starfunCR_o2
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	87	starfun_const_fun <-- starfunNat_const_fun, starfunNat2_const_fun, starfunC_const_fun, starfunRC_const_fun, starfunCR_const_fun
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	88	starfun_inverse <-- starfunNat_inverse, starfunC_inverse, starfunRC_inverse, starfunCR_inverse
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	89	starfun_eq <-- starfunNat_eq, starfunNat2_eq, starfunC_eq, starfunRC_eq, starfunCR_eq
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	90	starfun_eq_iff <-- starfunC_eq_iff, starfunRC_eq_iff, starfunCR_eq_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	91	starfun_Id <-- starfunC_Id
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	92	starfun_approx <-- starfunNat_approx, starfunCR_approx
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	93	starfun_capprox <-- starfunC_capprox, starfunRC_capprox
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	94	starfun_abs <-- starfunNat_rabs
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	95	starfun_lambda_cancel <-- starfunC_lambda_cancel, starfunCR_lambda_cancel, starfunRC_lambda_cancel
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	96	starfun_lambda_cancel2 <-- starfunC_lambda_cancel2, starfunCR_lambda_cancel2, starfunRC_lambda_cancel2
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	97	starfun_mult_HFinite_approx <-- starfunCR_mult_HFinite_capprox
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	98	starfun_mult_CFinite_capprox <-- starfunC_mult_CFinite_capprox, starfunRC_mult_CFinite_capprox
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	99	starfun_add_capprox <-- starfunC_add_capprox, starfunRC_add_capprox
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	100	starfun_add_approx <-- starfunCR_add_approx
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	101	starfun_inverse_inverse <-- starfunC_inverse_inverse
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	102	starfun_divide <-- starfunC_divide, starfunCR_divide, starfunRC_divide
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	103	starfun_n_congruent <-- starfunNat_n_congruent, starfunC_n_congruent
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	104	starfun_n <-- starfunNat_n, starfunC_n
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	105	starfun_n_mult <-- starfunNat_n_mult, starfunC_n_mult
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	106	starfun_n_add <-- starfunNat_n_add, starfunC_n_add
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	107	starfun_n_add_minus <-- starfunNat_n_add_minus
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	108	starfun_n_const_fun <-- starfunNat_n_const_fun, starfunC_n_const_fun
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	109	starfun_n_minus <-- starfunNat_n_minus, starfunC_n_minus
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	110	starfun_n_eq <-- starfunNat_n_eq, starfunC_n_eq
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	111
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	112	star_n_add <-- hypreal_add, hypnat_add, hcomplex_add
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	113	star_n_minus <-- hypreal_minus, hcomplex_minus
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	114	star_n_diff <-- hypreal_diff, hcomplex_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	115	star_n_mult <-- hypreal_mult, hcomplex_mult
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	116	star_n_inverse <-- hypreal_inverse, hcomplex_inverse
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	117	star_n_le <-- hypreal_le, hypnat_le
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	118	star_n_less <-- hypreal_less, hypnat_less
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	119	star_n_zero_num <-- hypreal_zero_num, hypnat_zero_num, hcomplex_zero_num
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	120	star_n_one_num <-- hypreal_one_num, hypnat_one_num, hcomplex_one_num
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	121	star_n_abs <-- hypreal_hrabs
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	122	star_n_divide <-- hcomplex_divide
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	123
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	124	star_of_add <-- hypreal_of_real_add
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	125	star_of_minus <-- hypreal_of_real_minus
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	126	star_of_diff <-- hypreal_of_real_diff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	127	star_of_mult <-- hypreal_of_real_mult
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	128	star_of_one <-- hypreal_of_real_one
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	129	star_of_zero <-- hypreal_of_real_zero
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	130	star_of_le <-- hypreal_of_real_le_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	131	star_of_less <-- hypreal_of_real_less_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	132	star_of_eq <-- hypreal_of_real_eq_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	133	star_of_inverse <-- hypreal_of_real_inverse
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	134	star_of_divide <-- hypreal_of_real_divide
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	135	star_of_of_nat <-- hypreal_of_real_of_nat
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	136	star_of_of_int <-- hypreal_of_real_of_int
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	137	star_of_number_of <-- hypreal_number_of
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	138	star_of_number_less <-- number_of_less_hypreal_of_real_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	139	star_of_number_le <-- number_of_le_hypreal_of_real_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	140	star_of_eq_number <-- hypreal_of_real_eq_number_of_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	141	star_of_less_number <-- hypreal_of_real_less_number_of_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	142	star_of_le_number <-- hypreal_of_real_le_number_of_iff
6e5815f4d770 list of constants and theorems whose names have been changed or merged huffman parents: diff changeset	143	star_of_power <-- hypreal_of_real_power

author	huffman
	Mon, 12 Sep 2005 23:27:12 +0200
changeset 17334	6e5815f4d770
child 17373	27509e72f29e
permissions	-rw-r--r--