#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
ddb3888b |
|
09-Aug-2016 |
nipkow <none@none> |
adapted ZF,FOL,CCL,LCF to modified splitter
|
#
4125d2fe |
|
28-Jul-2015 |
wenzelm <none@none> |
more explicit context;
|
#
cff2e75b |
|
08-Apr-2015 |
wenzelm <none@none> |
proper context for Object_Logic operations;
|
#
c97e9ad6 |
|
07-Mar-2015 |
wenzelm <none@none> |
clarified Drule.gen_all: observe context more carefully;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
#
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
#
2d556eb3 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
8aa502e5 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature; clarified context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
f21371f9 |
|
28-Nov-2011 |
wenzelm <none@none> |
avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
|
#
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
7bae4824 |
|
23-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
a9de3adb |
|
29-Jun-2011 |
wenzelm <none@none> |
tuned signature;
|
#
9c72c6e0 |
|
29-Jun-2011 |
wenzelm <none@none> |
simplified/unified Simplifier.mk_solver;
|
#
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
|
#
5585cb3d |
|
26-Apr-2011 |
wenzelm <none@none> |
modernized Clasimp setup;
|
#
7f6fd60f |
|
22-Apr-2011 |
wenzelm <none@none> |
simplified Data signature;
|
#
ebf09630 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning;
|
#
f1968c93 |
|
22-Apr-2011 |
wenzelm <none@none> |
modernized Quantifier1 simproc setup;
|
#
b4763bb2 |
|
21-Apr-2011 |
wenzelm <none@none> |
clarified simpset setup; discontinued unused old-style FOL_css;
|
#
f95e18b9 |
|
20-Dec-2010 |
wenzelm <none@none> |
proper identifiers for consts and types;
|
#
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
#
7cffb5dd |
|
17-Aug-2010 |
haftmann <none@none> |
more antiquotations
|
#
6bbc2f67 |
|
30-Apr-2010 |
wenzelm <none@none> |
removed some old comments;
|
#
fa5430f0 |
|
30-Apr-2010 |
wenzelm <none@none> |
proper context for rule_by_tactic;
|
#
b96c5111 |
|
29-Apr-2010 |
wenzelm <none@none> |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
#
aa047a26 |
|
19-Feb-2010 |
wenzelm <none@none> |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
#
2396d686 |
|
07-Feb-2010 |
wenzelm <none@none> |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
#
a2aef54e |
|
16-Oct-2009 |
wenzelm <none@none> |
explicitly qualify Drule.standard;
|
#
75401f7b |
|
15-Oct-2009 |
wenzelm <none@none> |
replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
|
#
4137057a |
|
24-Jul-2009 |
wenzelm <none@none> |
renamed functor SplitterFun to Splitter, require explicit theory;
|
#
92e775bc |
|
23-Jul-2009 |
wenzelm <none@none> |
more @{theory} antiquotations;
|
#
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
#
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
#
b305563f |
|
09-Jul-2009 |
wenzelm <none@none> |
removed obsolete CVS Ids;
|
#
1716138f |
|
20-Mar-2009 |
wenzelm <none@none> |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
#
5317e9bf |
|
17-Sep-2008 |
wenzelm <none@none> |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
#
56ac4f51 |
|
24-Jun-2008 |
wenzelm <none@none> |
ML_Antiquote.value;
|
#
1a1b9232 |
|
29-Mar-2008 |
wenzelm <none@none> |
purely functional setup of claset/simpset/clasimpset;
|
#
bbdf200a |
|
15-Mar-2008 |
wenzelm <none@none> |
eliminated out-of-scope proofs (cf. theory IFOL and FOL); proper antiquotations;
|
#
bdb79104 |
|
27-Apr-2007 |
wenzelm <none@none> |
removed obsolete induct/simp tactic;
|
#
6e5e9246 |
|
20-Jan-2007 |
wenzelm <none@none> |
added @{clasimpset};
|
#
fcd0176f |
|
26-Nov-2006 |
wenzelm <none@none> |
converted legacy ML scripts;
|
#
1f27d6b3 |
|
27-Jul-2006 |
wenzelm <none@none> |
tuned proofs;
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
89b1d8c9 |
|
31-Dec-2005 |
wenzelm <none@none> |
removed obsolete Provers/make_elim.ML;
|
#
dcc17ba3 |
|
01-Dec-2005 |
wenzelm <none@none> |
unfold_tac: static evaluation of simpset;
|
#
25da66f0 |
|
18-Oct-2005 |
wenzelm <none@none> |
Simplifier.theory_context;
|
#
f7fba198 |
|
17-Oct-2005 |
wenzelm <none@none> |
change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
#
dcefbda4 |
|
12-Sep-2005 |
haftmann <none@none> |
introduced new-style AList operations
|
#
593d5827 |
|
02-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
8b6756fc |
|
22-May-2005 |
wenzelm <none@none> |
Simplifier already setup in Pure;
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
1f05977e |
|
06-Aug-2002 |
wenzelm <none@none> |
sane interface for simprocs;
|
#
0cfe8696 |
|
15-May-2002 |
paulson <none@none> |
better simplification of trivial existential equalities
|
#
28b04eed |
|
21-Jan-2002 |
paulson <none@none> |
new simprules and classical rules
|
#
c7ecb97e |
|
15-Jan-2002 |
paulson <none@none> |
new theorem
|
#
7e01175e |
|
12-Jan-2002 |
wenzelm <none@none> |
renamed forall_elim_vars_safe to gen_all;
|
#
b8b69ab5 |
|
11-Jan-2002 |
wenzelm <none@none> |
replace gen_all by forall_elim_vars_safe;
|
#
ec1161a5 |
|
17-Dec-2001 |
nipkow <none@none> |
mods due to changed 1-point simprocs (quantifier1).
|
#
ab0b1481 |
|
03-Nov-2001 |
wenzelm <none@none> |
proper use of bind_thm(s);
|
#
3cb3797d |
|
14-Oct-2001 |
wenzelm <none@none> |
moved rulify to ObjectLogic;
|
#
f252e141 |
|
14-Oct-2001 |
wenzelm <none@none> |
eliminated atomize rules;
|
#
ecf9baa3 |
|
31-May-2001 |
oheimb <none@none> |
streamlined addIffs/delIffs, added warnings
|
#
d032b770 |
|
29-Mar-2001 |
nipkow <none@none> |
generalization of 1 point rules for ALL
|
#
83bcd811 |
|
10-Nov-2000 |
wenzelm <none@none> |
FOL_basic_ss: simprocs moved to FOL_ss;
|
#
f27b2ee7 |
|
07-Sep-2000 |
wenzelm <none@none> |
rulify setup;
|
#
02337f03 |
|
05-Sep-2000 |
wenzelm <none@none> |
iff declarations moved to clasimp.ML;
|
#
4d41c00b |
|
28-Aug-2000 |
wenzelm <none@none> |
cong setup now part of Simplifier;
|
#
baded603 |
|
12-Jul-2000 |
paulson <none@none> |
AddIffs now available for FOL, ZF
|
#
58b7525b |
|
31-Mar-2000 |
wenzelm <none@none> |
added cong atts;
|
#
eee93f23 |
|
15-Mar-2000 |
wenzelm <none@none> |
clasimp: include Splitter;
|
#
3115c3d5 |
|
21-Sep-1999 |
nipkow <none@none> |
Mod because of new solver interface.
|
#
649c6263 |
|
25-Aug-1999 |
wenzelm <none@none> |
proper bootstrap of IFOL/FOL theories and packages;
|
#
ed8201ed |
|
17-Mar-1999 |
wenzelm <none@none> |
Theory.sign_of;
|
#
cd6b66d9 |
|
12-Jan-1999 |
paulson <none@none> |
congruence rules finally use == instead of = and <->
|
#
c4500d3a |
|
24-Sep-1998 |
oheimb <none@none> |
simplified CLASIMP_DATA renamed mk_meta_eq to mk_eq introduced new mk_meta_eq, simplified addcongs and delcongs, introducing mk_meta_cong
|
#
d75e00ab |
|
18-Sep-1998 |
paulson <none@none> |
Pruning of parameters and True assumptions
|
#
954cf0ec |
|
12-Aug-1998 |
oheimb <none@none> |
minor adaption for SML/NJ
|
#
8e7a54b6 |
|
12-Aug-1998 |
oheimb <none@none> |
the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset
|
#
14345bc7 |
|
30-Jul-1998 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
623d3541 |
|
30-Jul-1998 |
wenzelm <none@none> |
functorized Clasimp module;
|
#
a1ab3f52 |
|
02-Jul-1998 |
paulson <none@none> |
HACKED declaration of addsplits
|
#
588c26e8 |
|
14-May-1998 |
oheimb <none@none> |
extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info
|
#
c660f140 |
|
03-Apr-1998 |
wenzelm <none@none> |
no open Simplifier;
|
#
ab1420d6 |
|
28-Feb-1998 |
nipkow <none@none> |
Splitters via named loopers.
|
#
786ad55a |
|
25-Feb-1998 |
oheimb <none@none> |
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset
|
#
cbae76ac |
|
25-Feb-1998 |
oheimb <none@none> |
changed wrapper mechanism of classical reasoner
|
#
f870a01c |
|
24-Dec-1997 |
paulson <none@none> |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
#
c951d1e2 |
|
03-Dec-1997 |
paulson <none@none> |
Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic
|
#
42255758 |
|
28-Nov-1997 |
paulson <none@none> |
addsplits now in FOL, ZF too
|
#
958f062e |
|
11-Nov-1997 |
oheimb <none@none> |
renamed split_prem_tac to split_asm_tac
|
#
16fa4a42 |
|
07-Nov-1997 |
oheimb <none@none> |
added split_prem_tac
|
#
a9ea8fb9 |
|
07-Nov-1997 |
oheimb <none@none> |
changed libraray function find to find_index_eq, currying it
|
#
43d488b9 |
|
02-Nov-1997 |
wenzelm <none@none> |
adapted to new implicit simpset;
|
#
6b3220b8 |
|
17-Oct-1997 |
paulson <none@none> |
New simprules imp_disj1,2 and some comments
|
#
9c98fba1 |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
#
80261fbc |
|
05-Aug-1997 |
berghofe <none@none> |
Moved functions from file "thy_data.ML".
|
#
b1651358 |
|
22-Jul-1997 |
wenzelm <none@none> |
standard congs;
|
#
f21d92b1 |
|
22-Jul-1997 |
paulson <none@none> |
Removal of the tactical STATE
|
#
3fc975cf |
|
15-May-1997 |
oheimb <none@none> |
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
|
#
1cce061e |
|
18-Mar-1997 |
nipkow <none@none> |
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
|
#
b9f6cc67 |
|
05-Mar-1997 |
paulson <none@none> |
Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
|
#
35628579 |
|
15-Feb-1997 |
oheimb <none@none> |
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss, safe_asm_more_full_simp_tac new addss (old version retained as unsafe_addss), new auto_tac (old version retained as unsafe_auto_tac), clasimpset with modification functions
|
#
8b74b342 |
|
09-Feb-1997 |
paulson <none@none> |
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
|
#
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
#
985eedce |
|
09-Oct-1996 |
paulson <none@none> |
Added the de Morgan laws (incl quantifier versions) to basic simpset
|
#
e5fceec2 |
|
08-Oct-1996 |
paulson <none@none> |
Addition of one-point quantifier rewrite rules
|
#
037e11f1 |
|
09-Sep-1996 |
paulson <none@none> |
Removal of (EX x. P) <-> P and (ALL x. P) <-> P from ex_simps and all_simps. as they are already in quant_simps.
|
#
036fc1fa |
|
05-Sep-1996 |
paulson <none@none> |
Introduction of miniscoping for FOL
|
#
0fd7fe50 |
|
19-Aug-1996 |
paulson <none@none> |
Added a lot of basic laws, from HOL/simpdata
|
#
73723b67 |
|
06-May-1996 |
berghofe <none@none> |
Added split_inside_tac.
|
#
8a318c3f |
|
29-Jan-1996 |
clasohm <none@none> |
expanded tabs
|
#
d209667e |
|
03-May-1995 |
lcp <none@none> |
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
|
#
0a333334 |
|
30-Mar-1995 |
lcp <none@none> |
Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)
|
#
4e3584ad |
|
08-Mar-1995 |
nipkow <none@none> |
Enforced partial evaluation of mk_case_split_tac.
|
#
2b6fe12f |
|
14-Dec-1994 |
lcp <none@none> |
conj_commute,disj_commute: new
|
#
0e8dcd7f |
|
30-Nov-1994 |
clasohm <none@none> |
added qed_goal for meta_iffD
|
#
ac1c4a46 |
|
24-Nov-1994 |
lcp <none@none> |
added blank line
|
#
67f7cfc0 |
|
17-Jun-1994 |
lcp <none@none> |
atomize: borrowed HOL version, which checks for both Trueprop and == as main connective (avoids using wildcard)
|
#
74db2614 |
|
24-May-1994 |
nipkow <none@none> |
Modified mk_meta_eq to leave meta-equlities on unchanged. Thus you may now add ==-thms to simpsets.
|
#
e499be24 |
|
13-May-1994 |
lcp <none@none> |
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the simplifier can rewrite premises, it can generate the premise False."
|
#
8e41a09e |
|
17-Mar-1994 |
lcp <none@none> |
FOL/simpdata: tidied FOL/simpdata/not_rews: moved the law "~(P|Q) <-> ~P & ~Q" from distrib_rews FOL/simpdata/cla_rews: added the law "~(P&Q) <-> ~P | ~Q"
|
#
d331910f |
|
05-Jan-1994 |
nipkow <none@none> |
updated solver of FOL_ss. see change of HOL/simpdata.ML
|
#
415c9c96 |
|
12-Oct-1993 |
nipkow <none@none> |
Added gen_all to simpdata.ML.
|
#
557ef142 |
|
16-Sep-1993 |
nipkow <none@none> |
defined local addcongs
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|