src/FOL/simpdata.ML
Sun, 19 Sep 2021 21:37:14 +0200 wenzelm clarified signature -- prefer antiquotations (with subtle change of exception content);
Sat, 11 Sep 2021 21:58:02 +0200 wenzelm more antiquotations;
Sat, 30 May 2020 11:48:35 +0000 haftmann specific atomization inert to later rule set modifications
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Tue, 09 Aug 2016 18:09:32 +0200 nipkow adapted ZF,FOL,CCL,LCF to modified splitter
Tue, 28 Jul 2015 20:59:39 +0200 wenzelm more explicit context;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Sat, 07 Mar 2015 21:32:31 +0100 wenzelm clarified Drule.gen_all: observe context more carefully;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
Thu, 30 Oct 2014 16:55:29 +0100 wenzelm eliminated aliases;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sun, 12 Jan 2014 14:32:22 +0100 wenzelm tuned signature;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Mon, 28 Nov 2011 17:05:41 +0100 wenzelm avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
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;
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;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Tue, 26 Apr 2011 21:49:39 +0200 wenzelm modernized Clasimp setup;
Fri, 22 Apr 2011 15:24:00 +0200 wenzelm simplified Data signature;
Fri, 22 Apr 2011 14:53:11 +0200 wenzelm misc tuning;
Fri, 22 Apr 2011 13:58:13 +0200 wenzelm modernized Quantifier1 simproc setup;
Fri, 22 Apr 2011 12:46:48 +0200 wenzelm clarified simpset setup;
Mon, 20 Dec 2010 16:44:33 +0100 wenzelm proper identifiers for consts and types;
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;
Tue, 17 Aug 2010 19:36:39 +0200 haftmann more antiquotations
Fri, 30 Apr 2010 21:10:57 +0200 wenzelm removed some old comments;
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Fri, 24 Jul 2009 21:34:37 +0200 wenzelm renamed functor SplitterFun to Splitter, require explicit theory;
Thu, 23 Jul 2009 23:12:21 +0200 wenzelm more @{theory} antiquotations;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Thu, 09 Jul 2009 22:09:58 +0200 wenzelm removed obsolete CVS Ids;
Fri, 20 Mar 2009 17:12:37 +0100 wenzelm Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Tue, 24 Jun 2008 19:43:14 +0200 wenzelm ML_Antiquote.value;
Sat, 29 Mar 2008 22:55:49 +0100 wenzelm purely functional setup of claset/simpset/clasimpset;
Sat, 15 Mar 2008 22:07:28 +0100 wenzelm eliminated out-of-scope proofs (cf. theory IFOL and FOL);
Fri, 27 Apr 2007 16:31:20 +0200 wenzelm removed obsolete induct/simp tactic;
Sat, 20 Jan 2007 14:09:11 +0100 wenzelm added @{clasimpset};
Sun, 26 Nov 2006 23:43:53 +0100 wenzelm converted legacy ML scripts;
Thu, 27 Jul 2006 13:43:00 +0200 wenzelm tuned proofs;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Sat, 31 Dec 2005 21:49:36 +0100 wenzelm removed obsolete Provers/make_elim.ML;
Thu, 01 Dec 2005 22:03:01 +0100 wenzelm unfold_tac: static evaluation of simpset;
Tue, 18 Oct 2005 17:59:25 +0200 wenzelm Simplifier.theory_context;
Mon, 17 Oct 2005 23:10:10 +0200 wenzelm change_claset/simpset;
Mon, 12 Sep 2005 18:20:32 +0200 haftmann introduced new-style AList operations
Tue, 02 Aug 2005 19:47:12 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Sun, 22 May 2005 16:51:07 +0200 wenzelm Simplifier already setup in Pure;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
less more (0) -100 -60 tip