isabelle: File revisions

src/HOL/Algebra/ringsimp.ML

2013-04-18	wenzelm	2013-04-18	simplifier uses proper Proof.context instead of historic type simpset;	file \| diff \| annotate
2012-04-23	wenzelm	2012-04-23	more standard method setup;	file \| diff \| annotate
2011-11-24	wenzelm	2011-11-24	modernized some old-style infix operations, which were left over from the time of ML proof scripts;	file \| diff \| annotate
2010-03-21	wenzelm	2010-03-21	standard headers;	file \| diff \| annotate
2010-02-27	wenzelm	2010-02-27	modernized structure Term_Ord;	file \| diff \| annotate
2009-11-08	wenzelm	2009-11-08	tuned;	file \| diff \| annotate
2009-11-08	wenzelm	2009-11-08	adapted Generic_Data, Proof_Data; tuned;	file \| diff \| annotate
2009-03-26	wenzelm	2009-03-26	simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;	file \| diff \| annotate
2009-03-15	wenzelm	2009-03-15	simplified attribute setup;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	simplified method setup;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	unified type Proof.method and pervasive METHOD combinators;	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
2007-10-09	wenzelm	2007-10-09	generic Syntax.pretty/string_of operations;	file \| diff \| annotate
2007-05-07	wenzelm	2007-05-07	simplified DataFun interfaces;	file \| diff \| annotate
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