src/HOL/Algebra/ringsimp.ML
Thu, 01 Feb 2018 15:31:25 +0100 wenzelm clarified signature: prefer proper order operation;
Thu, 01 Feb 2018 15:12:57 +0100 wenzelm tuned signature: more operations;
Wed, 29 Oct 2014 10:58:41 +0100 wenzelm modernized setup;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Mon, 23 Apr 2012 21:44:36 +0200 wenzelm more standard method setup;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 21 Mar 2010 17:12:31 +0100 wenzelm standard headers;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Sun, 08 Nov 2009 18:42:57 +0100 wenzelm tuned;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.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