#
c8257b0c |
|
07-Aug-2019 |
wenzelm <none@none> |
prefer named lemmas -- more compact proofterms;
|
#
ca7bf8cb |
|
06-Aug-2019 |
wenzelm <none@none> |
clarified signature; more careful treatment of implicit context;
|
#
fb065dfe |
|
04-Jun-2019 |
wenzelm <none@none> |
misc tuning and clarification, notably wrt. flow of context;
|
#
c93a1841 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature;
|
#
dfe0c24e |
|
13-Apr-2019 |
wenzelm <none@none> |
clarified: use existing Thm.dest_ctyp_fun (which is more strict);
|
#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
fad9031b |
|
19-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c66405dc |
|
31-Oct-2016 |
kuncar <none@none> |
always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)
|
#
53a62d5e |
|
12-Apr-2016 |
wenzelm <none@none> |
Type_Infer.object_logic controls improvement of type inference result;
|
#
8b4f2adf |
|
17-Feb-2016 |
blanchet <none@none> |
refactoring
|
#
a279bbf2 |
|
16-Dec-2015 |
wenzelm <none@none> |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
#
01f92480 |
|
08-Oct-2015 |
kuncar <none@none> |
new methods for debugging transfer and transfer_prover
|
#
ae530ff7 |
|
08-Oct-2015 |
kuncar <none@none> |
right parenthesization
|
#
7e21c646 |
|
01-Sep-2015 |
wenzelm <none@none> |
tuned -- avoid slightly odd @{cpat};
|
#
c2232610 |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature; clarified context;
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
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);
|
#
c431d096 |
|
03-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
#
65c57129 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
ac4c2cb4 |
|
11-Feb-2015 |
wenzelm <none@none> |
proper 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;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
c7ac8f9a |
|
18-Nov-2014 |
kuncar <none@none> |
tuned; store pred_simps
|
#
e12454e2 |
|
18-Nov-2014 |
kuncar <none@none> |
added pred_def, rel_eq_onp tuned
|
#
8049c47b |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
2b96dcb2 |
|
25-Apr-2014 |
wenzelm <none@none> |
make SML/NJ happier;
|
#
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
|