| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
5f64552a |
|
11-Jan-2016 |
wenzelm <none@none> |
eliminated old defs;
|
| #
c9f3da2d |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <->;
|
| #
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
e11de3a7 |
|
26-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
b0d49015 |
|
26-Jun-2015 |
wenzelm <none@none> |
more symbols;
eliminated alternative syntax;
|
| #
69b24741 |
|
26-Jun-2015 |
wenzelm <none@none> |
more symbols;
|
| #
403911ef |
|
26-Jun-2015 |
wenzelm <none@none> |
more symbols;
|
| #
8cc66666 |
|
27-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
f6e927dc |
|
24-Mar-2015 |
wenzelm <none@none> |
clarified case_tac fixes and context;
|
| #
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);
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
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;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
5267fff3 |
|
12-Oct-2011 |
wenzelm <none@none> |
modernized structure Induct_Tacs;
|
| #
9c72c6e0 |
|
29-Jun-2011 |
wenzelm <none@none> |
simplified/unified Simplifier.mk_solver;
|
| #
10eb7fb0 |
|
15-May-2011 |
wenzelm <none@none> |
simplified/unified method_setup/attribute_setup;
|
| #
666f74a4 |
|
13-May-2011 |
wenzelm <none@none> |
proper method_setup "split_idle";
|
| #
0cc9f7b7 |
|
12-May-2011 |
wenzelm <none@none> |
modernized dead code;
|
| #
5f711e87 |
|
12-May-2011 |
wenzelm <none@none> |
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
|
| #
8e423a47 |
|
12-May-2011 |
wenzelm <none@none> |
eliminated obsolete MI_css -- use current context directly;
|
| #
53ded129 |
|
20-Mar-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
216c8115 |
|
16-Jan-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
27ff3609 |
|
06-Sep-2010 |
wenzelm <none@none> |
more antiquotations;
|
| #
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
| #
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;
|
| #
ea407404 |
|
14-Jun-2008 |
wenzelm <none@none> |
proper context for tactics derived from res_inst_tac;
|
| #
667f1264 |
|
10-Jun-2008 |
wenzelm <none@none> |
case_split_tac (works without context);
|
| #
d0dc0ab4 |
|
09-Jun-2008 |
wenzelm <none@none> |
DatatypePackage.case_tac;
|
| #
bd98015c |
|
19-Mar-2008 |
wenzelm <none@none> |
more antiquotations;
|
| #
13c78537 |
|
07-Aug-2007 |
wenzelm <none@none> |
tuned ML setup;
|
| #
4a856837 |
|
01-Dec-2006 |
wenzelm <none@none> |
TLA: converted legacy ML scripts;
|
| #
f55bd273 |
|
07-Sep-2005 |
wenzelm <none@none> |
converted to Isar theory format;
|
| #
49f4684e |
|
05-Oct-2001 |
wenzelm <none@none> |
tuned;
|
| #
ace2eaf8 |
|
03-Aug-2000 |
wenzelm <none@none> |
tuned version by Stephan Merz (unbatchified etc.);
|
| #
0c0fa6ed |
|
08-Feb-1999 |
wenzelm <none@none> |
updated (Stephan Merz);
|
| #
8b3b3609 |
|
08-Oct-1997 |
wenzelm <none@none> |
A formalization of TLA in HOL -- by Stephan Merz;
|