| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
a64ec6cd |
|
08-Jul-2015 |
wenzelm <none@none> |
clarified 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);
|
| #
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;
|
| #
34700165 |
|
05-Mar-2015 |
wenzelm <none@none> |
tuned -- more explicit use of 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};
|
| #
8117bc8e |
|
02-Jun-2013 |
haftmann <none@none> |
denesting of functions
|
| #
de8113c2 |
|
01-Jun-2013 |
haftmann <none@none> |
make reification part of HOL
--HG--
rename : src/HOL/Tools/reflection.ML => src/HOL/Tools/reification.ML
extra : rebase_source : 16e93aafd01e25dc85b597f0e457983c2b9cfe1b
|