isabelle: File revisions

src/HOL/Algebra/ringsimp.ML

2007-04-11	haftmann	2007-04-11	canonical merge operations	file \| diff \| annotate
2006-11-29	wenzelm	2006-11-29	simplified method setup;	file \| diff \| annotate
2006-11-23	wenzelm	2006-11-23	prefer Proof.context over Context.generic; tuned;	file \| diff \| annotate
2006-09-15	wenzelm	2006-09-15	tuned;	file \| diff \| annotate
2006-08-08	haftmann	2006-08-08	abandoned equal_list in favor for eq_list	file \| diff \| annotate
2006-07-19	ballarin	2006-07-19	Reimplemented algebra method; now controlled by attribute.	file \| diff \| annotate
2006-07-14	ballarin	2006-07-14	Term.term_lpo takes order on terms rather than strings as argument.	file \| diff \| annotate
2006-06-20	ballarin	2006-06-20	Restructured locales with predicates: import is now an interpretation. New method intro_locales.	file \| diff \| annotate
2005-06-25	nipkow	2005-06-25	Changes due to new abel_cancel.ML	file \| diff \| annotate
2005-06-20	wenzelm	2005-06-20	get_thm(s): Name;	file \| diff \| annotate
2005-03-03	skalberg	2005-03-03	Move towards standard functions.	file \| diff \| annotate
2005-02-13	skalberg	2005-02-13	Deleted Library.option type.	file \| diff \| annotate
2005-01-24	berghofe	2005-01-24	Adapted to modified interface of PureThy.get_thm(s).	file \| diff \| annotate
2004-06-17	paulson	2004-06-17	removal of magmas and semigroups	file \| diff \| annotate
2004-02-19	ballarin	2004-02-19	New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.	file \| diff \| annotate
2003-04-30	ballarin	2003-04-30	Greatly extended CRing. Added Module.	file \| diff \| annotate
2003-03-14	ballarin	2003-03-14	Bugs fixed and operators finprod and finsum.	file \| diff \| annotate
2003-03-10	ballarin	2003-03-10	First distributed version of Group and Ring theory.	file \| diff \| annotate

isabelle

RSS Atom