isabelle: File revisions

src/HOL/OrderedGroup.thy

2009-10-30	haftmann	2009-10-30	tuned code setup	file \| diff \| annotate
2009-09-22	haftmann	2009-09-22	be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer	file \| diff \| annotate
2009-08-28	nipkow	2009-08-28	tuned proofs	file \| diff \| annotate
2009-08-28	nipkow	2009-08-28	Turned "x <= y ==> sup x y = y" (and relatives) into simp rules	file \| diff \| annotate
2009-07-20	haftmann	2009-07-20	merged	file \| diff \| annotate
2009-07-14	haftmann	2009-07-14	refinement of lattice classes	file \| diff \| annotate
2009-07-15	wenzelm	2009-07-15	more antiquotations;	file \| diff \| annotate
2009-07-02	wenzelm	2009-07-02	renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;	file \| diff \| annotate
2009-05-04	haftmann	2009-05-04	dropped duplicate lemma sum_nonneg_eq_zero_iff	file \| diff \| annotate
2009-04-28	haftmann	2009-04-28	lemma sum_nonneg_eq_zero_iff	file \| diff \| annotate
2009-03-23	huffman	2009-03-23	lemmas add_sign_intros	file \| diff \| annotate
2009-03-21	huffman	2009-03-21	move diff_eq_0_iff_eq into class locale context	file \| diff \| annotate
2009-02-14	huffman	2009-02-14	generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup	file \| diff \| annotate
2009-02-13	huffman	2009-02-13	add class cancel_comm_monoid_add	file \| diff \| annotate
2009-02-12	huffman	2009-02-12	add lemma add_nonneg_eq_0_iff	file \| diff \| annotate
2009-02-08	nipkow	2009-02-08	added noatps	file \| diff \| annotate
2009-01-28	nipkow	2009-01-28	removed spurious conflic msg	file \| diff \| annotate
2009-01-28	nipkow	2009-01-28	merged - resolving conflics	file \| diff \| annotate
2009-01-28	nipkow	2009-01-28	Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now	file \| diff \| annotate
2009-01-19	haftmann	2009-01-19	tuned proof	file \| diff \| annotate
2008-12-31	wenzelm	2008-12-31	moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;	file \| diff \| annotate
2008-11-17	haftmann	2008-11-17	tuned unfold_locales invocation	file \| diff \| annotate
2008-09-17	wenzelm	2008-09-17	back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;	file \| diff \| annotate
2008-09-04	huffman	2008-09-04	move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add	file \| diff \| annotate
2008-07-10	huffman	2008-07-10	by intro_locales -> ..	file \| diff \| annotate
2008-07-03	huffman	2008-07-03	move proofs of add_left_cancel and add_right_cancel into the correct locale	file \| diff \| annotate
2008-06-18	wenzelm	2008-06-18	simplified Abel_Cancel setup;	file \| diff \| annotate
2008-03-29	wenzelm	2008-03-29	replaced 'ML_setup' by 'ML';	file \| diff \| annotate
2008-02-15	haftmann	2008-02-15	*moved _reorient lemmas here**	file \| diff \| annotate
2008-01-30	haftmann	2008-01-30	idempotent semigroups	file \| diff \| annotate
2008-01-02	haftmann	2008-01-02	splitted class uminus from class minus	file \| diff \| annotate
2007-12-13	haftmann	2007-12-13	dropped ws	file \| diff \| annotate
2007-11-30	haftmann	2007-11-30	using intro_locales instead of unfold_locales if appropriate	file \| diff \| annotate
2007-11-06	haftmann	2007-11-06	*simplified specification of _abs class**	file \| diff \| annotate
2007-11-06	haftmann	2007-11-06	*renamed lordered__* to lordered__add_; further localization**	file \| diff \| annotate
2007-11-02	haftmann	2007-11-02	proper reinitialisation after subclass	file \| diff \| annotate
2007-10-30	haftmann	2007-10-30	continued localization	file \| diff \| annotate
2007-10-25	haftmann	2007-10-25	dropped redundancy	file \| diff \| annotate
2007-10-19	haftmann	2007-10-19	antisymmetry not a default intro rule any longer	file \| diff \| annotate
2007-10-19	haftmann	2007-10-19	98% localized	file \| diff \| annotate
2007-10-18	haftmann	2007-10-18	continued localization	file \| diff \| annotate
2007-10-16	haftmann	2007-10-16	global class syntax	file \| diff \| annotate
2007-09-29	haftmann	2007-09-29	proper syntax during class specification	file \| diff \| annotate
2007-08-21	haftmann	2007-08-21	moved ordered_ab_semigroup_add to OrderedGroup.thy	file \| diff \| annotate
2007-08-15	paulson	2007-08-15	ATP blacklisting is now in theory data, attribute noatp	file \| diff \| annotate
2007-08-03	wenzelm	2007-08-03	replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;	file \| diff \| annotate
2007-07-20	haftmann	2007-07-20	split class abs from class minus	file \| diff \| annotate
2007-06-23	nipkow	2007-06-23	tuned and renamed group_eq_simps and ring_eq_simps	file \| diff \| annotate
2007-06-14	wenzelm	2007-06-14	tuned proofs: avoid implicit prems;	file \| diff \| annotate
2007-06-01	haftmann	2007-06-01	localized	file \| diff \| annotate
2007-05-24	nipkow	2007-05-24	Introduced new classes monoid_add and group_add	file \| diff \| annotate
2007-05-17	haftmann	2007-05-17	canonical prefixing of class constants	file \| diff \| annotate
2007-05-17	huffman	2007-05-17	remove redundant instance declaration	file \| diff \| annotate
2007-03-29	haftmann	2007-03-29	dropped legacy ML bindings	file \| diff \| annotate
2007-03-20	haftmann	2007-03-20	dropped OrderedGroup.ML	file \| diff \| annotate
2007-03-16	haftmann	2007-03-16	adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy	file \| diff \| annotate
2007-03-09	haftmann	2007-03-09	stepping towards uniform lattice theory development in HOL	file \| diff \| annotate
2007-03-02	haftmann	2007-03-02	now using "class"	file \| diff \| annotate
2006-11-15	haftmann	2006-11-15	dropped dependency on sets	file \| diff \| annotate
2006-11-13	haftmann	2006-11-13	dropped Inductive dependency	file \| diff \| annotate

isabelle

RSS Atom