| #
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
| #
0c041064 |
|
04-Jun-2019 |
wenzelm <none@none> |
misc tuning and clarification, notably wrt. flow of context;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
ef845594 |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified signature;
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
dbbe37ca |
|
15-Jul-2015 |
traytel <none@none> |
{r,e,d,f}tac with proper context in BNF
|
| #
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
| #
f6ce425b |
|
27-Mar-2015 |
blanchet <none@none> |
more graceful failure if some of the involved BNFs have no data
|
| #
17332b93 |
|
16-Mar-2015 |
wenzelm <none@none> |
proper headers;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
b7bf58e6 |
|
03-Mar-2015 |
traytel <none@none> |
eliminated some clones of Proof_Context.cterm_of
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
e12454e2 |
|
18-Nov-2014 |
kuncar <none@none> |
added pred_def, rel_eq_onp tuned
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
bb4c3636 |
|
13-Oct-2014 |
wenzelm <none@none> |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
edde5141 |
|
08-Sep-2014 |
blanchet <none@none> |
made 'lifting' plugin more robust
|
| #
6bd76c01 |
|
04-Sep-2014 |
blanchet <none@none> |
pretend code generation is a ctr_sugar plugin
|
| #
625d35eb |
|
04-Sep-2014 |
blanchet <none@none> |
named interpretations
|
| #
ec4e6125 |
|
04-Sep-2014 |
blanchet <none@none> |
tuned size function generation
|
| #
3a5bbb8e |
|
03-Sep-2014 |
blanchet <none@none> |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
| #
ef2d5221 |
|
11-Aug-2014 |
traytel <none@none> |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
| #
6d2bb8d0 |
|
23-Apr-2014 |
kuncar <none@none> |
predicator simplification rules: support also partially specialized types e.g. 'a * nat
|
| #
e9e8c934 |
|
10-Apr-2014 |
kuncar <none@none> |
setup for Transfer and Lifting from BNF; tuned thm names
--HG--
rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML
|