| #
c1869c88 |
|
24-Jul-2015 |
wenzelm <none@none> |
proper context;
|
| #
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
8083303a |
|
23-Mar-2015 |
wenzelm <none@none> |
support 'for' fixes in rule_tac etc.;
|
| #
2d6c364b |
|
20-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
4e1305ff |
|
19-Mar-2015 |
wenzelm <none@none> |
more position information;
|
| #
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);
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
94314ed4 |
|
01-Mar-2012 |
haftmann <none@none> |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
| #
b26df718 |
|
13-Oct-2011 |
haftmann <none@none> |
tuned
--HG--
extra : rebase_source : b500c43fafaf3070bed198919b54e9771353c621
|
| #
14ffc3e9 |
|
13-May-2011 |
wenzelm <none@none> |
clarified map_simpset versus Simplifier.map_simpset_global;
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
5d2a8866 |
|
12-May-2011 |
wenzelm <none@none> |
prefer Proof.context over old-style clasimpset;
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
5f5d654c |
|
03-Jan-2010 |
paulson <none@none> |
removed legacy asm_lr_simp_tac
|
| #
a733ded7 |
|
20-Mar-2009 |
wenzelm <none@none> |
eliminated old Addsimps;
|
| #
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;
|
| #
99b04075 |
|
03-Aug-2007 |
wenzelm <none@none> |
misc cleanup of ML bindings (for multihreading);
|
| #
9f120b31 |
|
05-Dec-2006 |
wenzelm <none@none> |
removed legacy ML bindings;
|
| #
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
| #
1674bc09 |
|
31-Jan-2003 |
paulson <none@none> |
conversion to new-style theories and tidying
|
| #
8671b95c |
|
30-Jan-2003 |
paulson <none@none> |
conversion of UNITY theories to new-style
|
| #
06317d69 |
|
30-Jan-2003 |
paulson <none@none> |
converting more UNITY theories to new-style
|
| #
b4eac3e6 |
|
29-Jan-2003 |
paulson <none@none> |
converted more UNITY theories to new-style
|
| #
e1895cc3 |
|
29-Jan-2003 |
paulson <none@none> |
converting UNITY to new-style theories
|
| #
71fec134 |
|
24-Jan-2003 |
paulson <none@none> |
More conversion of UNITY to Isar new-style theories
|