| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
8083303a |
|
23-Mar-2015 |
wenzelm <none@none> |
support 'for' fixes in rule_tac etc.;
|
| #
2d6c364b |
|
20-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
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
|
| #
a1be1ce9 |
|
09-Sep-2014 |
blanchet <none@none> |
rename_tac'd scripts
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
64579d07 |
|
24-May-2013 |
haftmann <none@none> |
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
--HG--
extra : rebase_source : bce13f16528e99c8a7a9be429782c1f1d3c29d49
|
| #
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";
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
8a93cad0 |
|
30-Mar-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
8ecfd549 |
|
12-Jan-2011 |
wenzelm <none@none> |
eliminated global prems;
|
| #
9e4cf179 |
|
28-Nov-2010 |
nipkow <none@none> |
gave more standard finite set rules simp and intro attribute
|
| #
27ff3609 |
|
06-Sep-2010 |
wenzelm <none@none> |
more antiquotations;
|
| #
6bc0017f |
|
02-Mar-2010 |
wenzelm <none@none> |
cleanup type translations;
|
| #
2251533a |
|
20-Mar-2009 |
wenzelm <none@none> |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
| #
29ecfaef |
|
25-Jun-2008 |
wenzelm <none@none> |
modernized specifications;
|
| #
fe16ec1f |
|
16-Jun-2008 |
wenzelm <none@none> |
pervasive RuleInsts;
|
| #
ea407404 |
|
14-Jun-2008 |
wenzelm <none@none> |
proper context for tactics derived from res_inst_tac;
|
| #
95ee7518 |
|
21-Jul-2007 |
wenzelm <none@none> |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
| #
7b63d2a6 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
745db1a3 |
|
26-Jul-2006 |
webertj <none@none> |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
| #
148dff9b |
|
06-Jun-2006 |
wenzelm <none@none> |
removed obsolete ML files;
|
| #
c790252e |
|
17-Sep-2005 |
wenzelm <none@none> |
converted to Isar theory format;
|
| #
9a40d08d |
|
09-Jan-2001 |
nipkow <none@none> |
*** empty log message ***
|
| #
2aabe693 |
|
31-Jan-2000 |
oheimb <none@none> |
added IMPP to HOL
|