#
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
#
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
1ff366c9 |
|
13-Dec-2008 |
berghofe <none@none> |
Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.
|
#
2932189d |
|
22-May-2008 |
urbanc <none@none> |
made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct
|
#
f09e21bc |
|
14-Apr-2008 |
wenzelm <none@none> |
removed duplicate lemmas;
|
#
cd5ecf2a |
|
12-Mar-2008 |
urbanc <none@none> |
tuned
|
#
5a64f8c1 |
|
31-Dec-2007 |
urbanc <none@none> |
tuned proofs and comments
|
#
9ad1fb76 |
|
14-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems;
|
#
8dcc70e7 |
|
11-Jun-2007 |
chaieb <none@none> |
tuned Proof
|
#
6384e974 |
|
01-May-2007 |
urbanc <none@none> |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
#
228c94bd |
|
06-Mar-2007 |
urbanc <none@none> |
major update of the nominal package; there is now an infrastructure for equivariance lemmas which eases definitions of nominal functions
|
#
ef19da37 |
|
27-Nov-2006 |
urbanc <none@none> |
adapted function definitions to new syntax
|
#
648c3850 |
|
22-Oct-2006 |
berghofe <none@none> |
Adapted to changes in FCBs.
|
#
66f838a8 |
|
18-Oct-2006 |
urbanc <none@none> |
cleaning up
|
#
927b5ff8 |
|
18-Aug-2006 |
urbanc <none@none> |
modified to use the characteristic equations
|
#
cbda7798 |
|
17-Aug-2006 |
urbanc <none@none> |
used the recursion combinator for the height and substitution function
|
#
bda4ce4f |
|
01-Jun-2006 |
urbanc <none@none> |
added an example suggested by D. Wang on the PoplMark-mailing list; it shows how the height of an alpha-equated lambda term interacts with capture-avoiding substitution
|