#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
#
c05194cb |
|
16-Aug-2015 |
wenzelm <none@none> |
tuned signature;
|
#
9e84b8bf |
|
02-Jun-2015 |
wenzelm <none@none> |
tuned;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
78821146 |
|
27-Aug-2014 |
wenzelm <none@none> |
more explicit Method.modifier with reported position;
|
#
e1988415 |
|
19-Aug-2014 |
wenzelm <none@none> |
added PARALLEL_ALLGOALS convenience;
|
#
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
d8ea875e |
|
12-Apr-2013 |
wenzelm <none@none> |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
#
dca616a7 |
|
17-Nov-2012 |
wenzelm <none@none> |
tuned;
|
#
09e81af1 |
|
17-Nov-2012 |
wenzelm <none@none> |
tuned signature;
|
#
92ff2eb0 |
|
23-May-2012 |
wenzelm <none@none> |
discontinued obsolete method fastsimp / tactic fast_simp_tac;
|
#
9fa04411 |
|
06-Nov-2011 |
wenzelm <none@none> |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
303e5a84 |
|
09-Jun-2011 |
wenzelm <none@none> |
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;
|
#
4c8d3d35 |
|
14-May-2011 |
wenzelm <none@none> |
discontinued old / unused addss' (cf. 57f364d1d3b2);
|
#
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
|
#
2f28aab2 |
|
13-May-2011 |
wenzelm <none@none> |
simplified clasimpset declarations -- prefer attributes;
|
#
ede4087e |
|
26-Apr-2011 |
wenzelm <none@none> |
tuned;
|
#
5585cb3d |
|
26-Apr-2011 |
wenzelm <none@none> |
modernized Clasimp setup;
|
#
aa7cb91d |
|
16-Apr-2011 |
wenzelm <none@none> |
PARALLEL_GOALS for simplification within auto_tac;
|
#
3a3bd1e4 |
|
05-Jul-2010 |
paulson <none@none> |
Unification (flexflex) bug fix; making "auto" deterministic
|
#
7a6b0131 |
|
17-May-2010 |
wenzelm <none@none> |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
|
#
bcdab2e1 |
|
30-Apr-2010 |
wenzelm <none@none> |
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
|
#
906be7a0 |
|
06-Mar-2010 |
wenzelm <none@none> |
eliminated Args.bang_facts (legacy feature);
|
#
1f5693a0 |
|
01-Nov-2009 |
wenzelm <none@none> |
modernized structure Context_Rules;
|
#
222e372a |
|
02-Oct-2009 |
wenzelm <none@none> |
eliminated dead code;
|
#
9bf7f277 |
|
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;
|
#
1716138f |
|
20-Mar-2009 |
wenzelm <none@none> |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
#
e2bdfca5 |
|
15-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
#
ca494c06 |
|
15-Mar-2009 |
wenzelm <none@none> |
simplified attribute setup;
|
#
da802918 |
|
13-Mar-2009 |
wenzelm <none@none> |
eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
|
#
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
d647eb14 |
|
01-Mar-2009 |
wenzelm <none@none> |
use long names for old-style fold combinators;
|
#
c80b3e70 |
|
09-Aug-2008 |
wenzelm <none@none> |
unified Args.T with OuterLex.token, renamed some operations;
|
#
e448476e |
|
29-Mar-2008 |
wenzelm <none@none> |
purely functional setup of claset/simpset/clasimpset; tuned signature;
|
#
be076d56 |
|
27-Mar-2008 |
wenzelm <none@none> |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
#
11a4159e |
|
19-Jan-2007 |
wenzelm <none@none> |
moved ML context stuff to from Context to ML_Context;
|
#
da6f4750 |
|
30-Dec-2006 |
wenzelm <none@none> |
removed obsolete name_hint handling;
|
#
dc9356ab |
|
08-Dec-2006 |
paulson <none@none> |
removed use of put_name_hint, as the ATP linkup no longer needs this
|
#
b5dac97b |
|
04-Dec-2006 |
wenzelm <none@none> |
thm/prf: separate official name vs. additional tags;
|
#
acdc5889 |
|
21-Jan-2006 |
wenzelm <none@none> |
simplified type attribute;
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
ab6437ef |
|
14-Jan-2006 |
wenzelm <none@none> |
generic attributes;
|
#
98a084a4 |
|
10-Jan-2006 |
wenzelm <none@none> |
generic attributes; added low-level modifiers from Pure/context_rules.ML;
|
#
89b1d8c9 |
|
31-Dec-2005 |
wenzelm <none@none> |
removed obsolete Provers/make_elim.ML;
|
#
0e080962 |
|
20-Dec-2005 |
paulson <none@none> |
modified suffix for [iff] attribute
|
#
34e8a702 |
|
17-Oct-2005 |
wenzelm <none@none> |
functor: no Simplifier argument; export change_clasimpset;
|
#
fff82f5e |
|
16-Aug-2005 |
paulson <none@none> |
classical rules must have names for ATP integration
|
#
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.
|
#
0d9b3ba0 |
|
11-Jul-2004 |
wenzelm <none@none> |
local_cla/simpset_of;
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
b4143277 |
|
30-Sep-2002 |
berghofe <none@none> |
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
|
#
9b561ab8 |
|
05-Mar-2002 |
wenzelm <none@none> |
iff: conditional rules declared as ``unsafe'';
|
#
58a4dbbe |
|
04-Dec-2001 |
wenzelm <none@none> |
iff?: refer to Pure/ContextRules;
|
#
25d9df76 |
|
23-Oct-2001 |
wenzelm <none@none> |
iff: always rotate prems;
|
#
f42bd677 |
|
09-Aug-2001 |
oheimb <none@none> |
corrected semantics of [iff] concerning rules with premises
|
#
d642f1fd |
|
05-Aug-2001 |
paulson <none@none> |
removed the warning from [iff]
|
#
ecf9baa3 |
|
31-May-2001 |
oheimb <none@none> |
streamlined addIffs/delIffs, added warnings
|
#
34904322 |
|
23-Feb-2001 |
oheimb <none@none> |
renamed addaltern to addafter, addSaltern to addSafter
|
#
07b92609 |
|
07-Jan-2001 |
wenzelm <none@none> |
CHANGED_PROP;
|
#
888c6fe2 |
|
24-Oct-2000 |
wenzelm <none@none> |
added clasimpset: unit -> clasimpset;
|
#
c5bd6429 |
|
19-Sep-2000 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
897d2b7a |
|
19-Sep-2000 |
wenzelm <none@none> |
added iff_add_global', iff_add_local' (syntax "iff?"); tuned;
|
#
2b4b27df |
|
13-Sep-2000 |
wenzelm <none@none> |
Args.addN, Args.delN;
|
#
725596cb |
|
07-Sep-2000 |
wenzelm <none@none> |
tuned msg;
|
#
9cef9f77 |
|
05-Sep-2000 |
wenzelm <none@none> |
added 'iff' declarations;
|
#
0f74409d |
|
02-Sep-2000 |
wenzelm <none@none> |
added "slowsimp", "bestsimp";
|
#
e28a7585 |
|
31-Aug-2000 |
wenzelm <none@none> |
auto method: opt args; tuned;
|
#
447803ce |
|
14-Aug-2000 |
wenzelm <none@none> |
added "fastsimp"; fixed "clarsimp": CHANGED;
|
#
62c04949 |
|
02-Aug-2000 |
wenzelm <none@none> |
export get_local_clasimpset, clasimp_modifiers;
|
#
9571e132 |
|
24-Jul-2000 |
wenzelm <none@none> |
added clarsimp method;
|
#
e75a5749 |
|
21-Jul-2000 |
oheimb <none@none> |
strengthened force_tac by using new first_best_tac
|
#
2dcc993f |
|
31-Mar-2000 |
wenzelm <none@none> |
added change_global/local_css;
|
#
fefaf775 |
|
15-Mar-2000 |
wenzelm <none@none> |
include Splitter.split_modifiers;
|
#
99396692 |
|
28-Jan-2000 |
wenzelm <none@none> |
HEADGOAL;
|
#
7fca48f4 |
|
27-Jan-2000 |
wenzelm <none@none> |
replaced FIRSTGOAL by FINDGOAL (backtracking!);
|
#
21474e5c |
|
27-Oct-1999 |
oheimb <none@none> |
clarsimp_tac now copes with the (unwanted) case that the simplifier splits the goal
|
#
a077d509 |
|
21-Sep-1999 |
wenzelm <none@none> |
setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts;
|
#
35269c25 |
|
02-Sep-1999 |
wenzelm <none@none> |
renamed improper method 'clarsimp' to 'clarsimp_tac';
|
#
63a7e2c7 |
|
01-Sep-1999 |
wenzelm <none@none> |
Method.insert_tac;
|
#
dd0f926f |
|
30-Aug-1999 |
wenzelm <none@none> |
auto: CHANGED;
|
#
195525f7 |
|
18-Aug-1999 |
wenzelm <none@none> |
Method.modifier;
|
#
0ccc7274 |
|
02-Aug-1999 |
wenzelm <none@none> |
tuned;
|
#
24d028b1 |
|
30-Jul-1999 |
wenzelm <none@none> |
eliminated METHOD0 in favour of same_tac;
|
#
e5b7576c |
|
29-Nov-1998 |
wenzelm <none@none> |
method brute_force = ALLGOALS force_tac;
|
#
2147f6a7 |
|
18-Nov-1998 |
wenzelm <none@none> |
method setup;
|
#
cfc9c20c |
|
23-Oct-1998 |
oheimb <none@none> |
corrected auto_tac (applications of unsafe wrappers) by correcting (and simplifying) nodup_depth_tac
|
#
d2c07750 |
|
25-Sep-1998 |
paulson <none@none> |
deleted illegal "op"
|
#
e898985a |
|
24-Sep-1998 |
oheimb <none@none> |
removed addcongs2 and delcongs2 simplified CLASIMP_DATA
|
#
219bcf11 |
|
21-Sep-1998 |
oheimb <none@none> |
improved addbefore and addSbefore improved mechanism for unsafe wrappers
|
#
a44b4b2e |
|
11-Sep-1998 |
oheimb <none@none> |
added clarsimp_tac and Clarsimp_tac
|
#
623d3541 |
|
30-Jul-1998 |
wenzelm <none@none> |
functorized Clasimp module;
|
#
c61eafb9 |
|
02-May-1998 |
wenzelm <none@none> |
added CLASIMPSET(') tacticals;
|
#
0a468db7 |
|
01-May-1998 |
oheimb <none@none> |
Auto_tac: now uses enhanced version of asm_full_simp_tac, Force_tac: replaced fast_tac by best_tac
|
#
85fa2b4d |
|
10-Mar-1998 |
oheimb <none@none> |
renamed smart_tac to force_tac, slight improvement of force_tac
|
#
7fcf96c1 |
|
26-Feb-1998 |
oheimb <none@none> |
added smart_tac
|
#
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
|