| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sun, 12 Jan 2014 14:32:22 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 17:05:41 +0100 |
wenzelm |
avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 21:49:39 +0200 |
wenzelm |
modernized Clasimp setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 15:24:00 +0200 |
wenzelm |
simplified Data signature;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 14:53:11 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 13:58:13 +0200 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 12:46:48 +0200 |
wenzelm |
clarified simpset setup;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 19:36:39 +0200 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 21:10:57 +0200 |
wenzelm |
removed some old comments;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 18:06:29 +0200 |
wenzelm |
proper context for rule_by_tactic;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:34:37 +0200 |
wenzelm |
renamed functor SplitterFun to Splitter, require explicit theory;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 23:12:21 +0200 |
wenzelm |
more @{theory} antiquotations;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:09:58 +0200 |
wenzelm |
removed obsolete CVS Ids;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:14 +0200 |
wenzelm |
ML_Antiquote.value;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 22:07:28 +0100 |
wenzelm |
eliminated out-of-scope proofs (cf. theory IFOL and FOL);
|
file |
diff |
annotate
|
| Fri, 27 Apr 2007 16:31:20 +0200 |
wenzelm |
removed obsolete induct/simp tactic;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:09:11 +0100 |
wenzelm |
added @{clasimpset};
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 23:43:53 +0100 |
wenzelm |
converted legacy ML scripts;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:36 +0100 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 22:03:01 +0100 |
wenzelm |
unfold_tac: static evaluation of simpset;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:25 +0200 |
wenzelm |
Simplifier.theory_context;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:10 +0200 |
wenzelm |
change_claset/simpset;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 18:20:32 +0200 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
| Tue, 02 Aug 2005 19:47:12 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Wed, 15 May 2002 10:42:32 +0200 |
paulson |
better simplification of trivial existential equalities
|
file |
diff |
annotate
|
| Mon, 21 Jan 2002 14:47:55 +0100 |
paulson |
new simprules and classical rules
|
file |
diff |
annotate
|
| Tue, 15 Jan 2002 15:07:41 +0100 |
paulson |
new theorem
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
| Fri, 11 Jan 2002 14:53:30 +0100 |
wenzelm |
replace gen_all by forall_elim_vars_safe;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2001 14:27:18 +0100 |
nipkow |
mods due to changed 1-point simprocs (quantifier1).
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 18:42:38 +0100 |
wenzelm |
proper use of bind_thm(s);
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:15:07 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 19:59:55 +0200 |
wenzelm |
eliminated atomize rules;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:02 +0200 |
oheimb |
streamlined addIffs/delIffs, added warnings
|
file |
diff |
annotate
|
| Thu, 29 Mar 2001 13:59:54 +0200 |
nipkow |
generalization of 1 point rules for ALL
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:01:33 +0100 |
wenzelm |
FOL_basic_ss: simprocs moved to FOL_ss;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:49:19 +0200 |
wenzelm |
rulify setup;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:46:36 +0200 |
wenzelm |
iff declarations moved to clasimp.ML;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:55:31 +0200 |
wenzelm |
cong setup now part of Simplifier;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 12:56:42 +0200 |
paulson |
AddIffs now available for FOL, ZF
|
file |
diff |
annotate
|
| Fri, 31 Mar 2000 22:22:23 +0200 |
wenzelm |
added cong atts;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:42:54 +0100 |
wenzelm |
clasimp: include Splitter;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 19:11:07 +0200 |
nipkow |
Mod because of new solver interface.
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 20:45:19 +0200 |
wenzelm |
proper bootstrap of IFOL/FOL theories and packages;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 12:08:51 +0100 |
paulson |
congruence rules finally use == instead of = and <->
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 17:18:33 +0200 |
oheimb |
simplified CLASIMP_DATA
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 14:34:06 +0200 |
paulson |
Pruning of parameters and True assumptions
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 17:40:18 +0200 |
oheimb |
minor adaption for SML/NJ
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:21:18 +0200 |
oheimb |
the splitter is now defined as a functor
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 19:18:50 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 19:02:52 +0200 |
wenzelm |
functorized Clasimp module;
|
file |
diff |
annotate
|
| Thu, 02 Jul 1998 17:56:06 +0200 |
paulson |
HACKED declaration of addsplits
|
file |
diff |
annotate
|
| Thu, 14 May 1998 16:50:09 +0200 |
oheimb |
extended addsplits and delsplits to handle also split rules for assumptions
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 12:29:07 +0200 |
wenzelm |
no open Simplifier;
|
file |
diff |
annotate
|
| Sat, 28 Feb 1998 15:41:17 +0100 |
nipkow |
Splitters via named loopers.
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 20:25:27 +0100 |
oheimb |
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 15:45:32 +0100 |
oheimb |
changed wrapper mechanism of classical reasoner
|
file |
diff |
annotate
|
| Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 10:48:16 +0100 |
paulson |
Instantiated the one-point-rule quantifier simpprocs for FOL
|
file |
diff |
annotate
|
| Fri, 28 Nov 1997 10:54:13 +0100 |
paulson |
addsplits now in FOL, ZF too
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 12:23:37 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 18:05:25 +0100 |
oheimb |
added split_prem_tac
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:28:01 +0100 |
wenzelm |
adapted to new implicit simpset;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 10:57:48 +0200 |
paulson |
New simprules imp_disj1,2 and some comments
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 15:52:12 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 00:41:40 +0200 |
berghofe |
Moved functions from file "thy_data.ML".
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 12:54:49 +0200 |
wenzelm |
standard congs;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:12:55 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Thu, 15 May 1997 15:51:09 +0200 |
oheimb |
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
|
file |
diff |
annotate
|
| Tue, 18 Mar 1997 08:43:26 +0100 |
nipkow |
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
|
file |
diff |
annotate
|
| Wed, 05 Mar 1997 10:07:04 +0100 |
paulson |
Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:43:27 +0100 |
oheimb |
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
|
file |
diff |
annotate
|
| Mon, 10 Feb 1997 12:31:54 +0100 |
paulson |
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Wed, 09 Oct 1996 13:36:17 +0200 |
paulson |
Added the de Morgan laws (incl quantifier versions) to basic simpset
|
file |
diff |
annotate
|
| Tue, 08 Oct 1996 10:17:50 +0200 |
paulson |
Addition of one-point quantifier rewrite rules
|
file |
diff |
annotate
|
| Mon, 09 Sep 1996 10:59:32 +0200 |
paulson |
Removal of (EX x. P) <-> P and (ALL x. P) <-> P
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 18:28:01 +0200 |
paulson |
Introduction of miniscoping for FOL
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:20:37 +0200 |
paulson |
Added a lot of basic laws, from HOL/simpdata
|
file |
diff |
annotate
|
| Mon, 06 May 1996 15:21:05 +0200 |
berghofe |
Added split_inside_tac.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:58:15 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 03 May 1995 13:35:09 +0200 |
lcp |
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
|
file |
diff |
annotate
|
| Thu, 30 Mar 1995 13:36:00 +0200 |
lcp |
Defined addss to perform simplification in a claset.
|
file |
diff |
annotate
|
| Wed, 08 Mar 1995 14:01:08 +0100 |
nipkow |
Enforced partial evaluation of mk_case_split_tac.
|
file |
diff |
annotate
|
| Wed, 14 Dec 1994 16:48:36 +0100 |
lcp |
conj_commute,disj_commute: new
|
file |
diff |
annotate
|
| Wed, 30 Nov 1994 13:18:42 +0100 |
clasohm |
added qed_goal for meta_iffD
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 00:02:37 +0100 |
lcp |
added blank line
|
file |
diff |
annotate
|
| Fri, 17 Jun 1994 17:49:03 +0200 |
lcp |
atomize: borrowed HOL version, which checks for both Trueprop
|
file |
diff |
annotate
|
| Tue, 24 May 1994 09:04:03 +0200 |
nipkow |
Modified mk_meta_eq to leave meta-equlities on unchanged.
|
file |
diff |
annotate
|
| Fri, 13 May 1994 11:25:55 +0200 |
lcp |
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
|
file |
diff |
annotate
|
| Thu, 17 Mar 1994 13:54:50 +0100 |
lcp |
FOL/simpdata: tidied
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:41:37 +0100 |
nipkow |
updated solver of FOL_ss. see change of HOL/simpdata.ML
|
file |
diff |
annotate
|
| Tue, 12 Oct 1993 13:39:35 +0100 |
nipkow |
Added gen_all to simpdata.ML.
|
file |
diff |
annotate
|