src/HOL/Algebra/ringsimp.ML
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Wed, 11 Apr 2007 08:28:15 +0200 haftmann canonical merge operations
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Thu, 23 Nov 2006 22:38:29 +0100 wenzelm prefer Proof.context over Context.generic;
Fri, 15 Sep 2006 22:56:08 +0200 wenzelm tuned;
Tue, 08 Aug 2006 08:18:59 +0200 haftmann abandoned equal_list in favor for eq_list
Wed, 19 Jul 2006 19:25:58 +0200 ballarin Reimplemented algebra method; now controlled by attribute.
Fri, 14 Jul 2006 14:37:15 +0200 ballarin Term.term_lpo takes order on terms rather than strings as argument.
Tue, 20 Jun 2006 15:53:44 +0200 ballarin Restructured locales with predicates: import is now an interpretation.
Sat, 25 Jun 2005 16:06:17 +0200 nipkow Changes due to new abel_cancel.ML
Mon, 20 Jun 2005 22:13:59 +0200 wenzelm get_thm(s): Name;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:16:57 +0100 berghofe Adapted to modified interface of PureThy.get_thm(s).
Thu, 17 Jun 2004 17:18:30 +0200 paulson removal of magmas and semigroups
Thu, 19 Feb 2004 16:44:21 +0100 ballarin New lemmas about inversion of restricted functions.
Wed, 30 Apr 2003 10:01:35 +0200 ballarin Greatly extended CRing. Added Module.
Fri, 14 Mar 2003 18:00:16 +0100 ballarin Bugs fixed and operators finprod and finsum.
Mon, 10 Mar 2003 17:25:34 +0100 ballarin First distributed version of Group and Ring theory.
less more (0) tip