src/ZF/arith_data.ML
Tue, 28 Sep 2021 17:09:05 +0200 wenzelm tuned antiquotations;
Tue, 21 Sep 2021 13:14:18 +0200 wenzelm clarified antiquotations;
Sun, 19 Sep 2021 21:37:14 +0200 wenzelm clarified signature -- prefer antiquotations (with subtle change of exception content);
Sun, 19 Sep 2021 20:47:16 +0200 wenzelm unused;
Sat, 11 Sep 2021 22:38:41 +0200 wenzelm more antiquotations;
Sat, 11 Sep 2021 22:02:12 +0200 wenzelm more antiquotations;
Tue, 06 Aug 2019 16:13:59 +0200 wenzelm tuned;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 11 Feb 2015 11:18:36 +0100 wenzelm proper context;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 30 Oct 2014 16:55:29 +0100 wenzelm eliminated aliases;
Mon, 11 Nov 2013 20:50:12 +0100 wenzelm tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sat, 17 Sep 2011 15:08:55 +0200 haftmann dropped unused argument – avoids problem with SML/NJ
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Mon, 20 Dec 2010 16:44:33 +0100 wenzelm proper identifiers for consts and types;
Thu, 02 Dec 2010 16:04:22 +0100 wenzelm renamed trace_simp to simp_trace, and debug_simp to simp_debug;
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Wed, 18 Aug 2010 12:08:21 +0200 haftmann more antiquotations
Sun, 28 Feb 2010 22:30:51 +0100 wenzelm more antiquotations;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Thu, 23 Jul 2009 23:12:21 +0200 wenzelm more @{theory} antiquotations;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Sat, 15 Mar 2008 22:07:26 +0100 wenzelm proper antiquotations;
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Sat, 05 Aug 2006 14:52:57 +0200 wenzelm tuned;
Wed, 12 Jul 2006 21:19:14 +0200 wenzelm simplified prove_conv;
Sat, 08 Jul 2006 12:54:30 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
Sat, 11 Mar 2006 21:23:10 +0100 wenzelm got rid of type Sign.sg;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Thu, 01 Dec 2005 22:04:27 +0100 wenzelm simprocs: static evaluation of simpset;
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Mon, 17 Oct 2005 23:10:15 +0200 wenzelm Simplifier.inherit_context instead of Simplifier.inherit_bounds;
Mon, 01 Aug 2005 19:20:26 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids
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.
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Thu, 08 Aug 2002 23:52:55 +0200 wenzelm tuned;
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Sat, 29 Jun 2002 21:33:06 +0200 paulson conversion of many files to Isar format
Thu, 16 May 2002 09:16:22 +0200 paulson converting Ordinal.ML to Isar format
Thu, 09 May 2002 17:51:19 +0200 paulson fixed simproc bug
Thu, 15 Nov 2001 18:18:17 +0100 wenzelm no handle ERROR;
Sat, 10 Nov 2001 16:25:17 +0100 wenzelm use Tactic.prove;
Wed, 06 Sep 2000 11:48:51 +0200 paulson bug fix for arithmetic simprocs (nat & int)
Fri, 18 Aug 2000 12:34:48 +0200 paulson simproc bug fix: only TYPING assumptions are given to the simplifier
Thu, 10 Aug 2000 11:27:34 +0200 paulson installation of cancellation simprocs for the integers
Mon, 07 Aug 2000 10:29:54 +0200 paulson instantiated Cancel_Numerals for "nat" in ZF
less more (0) tip