#
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;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
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
|
#
ffa009b0 |
|
11-Jul-2007 |
berghofe <none@none> |
Renamed inductive2 to inductive.
|
#
6384e974 |
|
01-May-2007 |
urbanc <none@none> |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
#
dbad4a37 |
|
28-Mar-2007 |
urbanc <none@none> |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
#
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
|
#
bc65205f |
|
07-Feb-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
c14736f9 |
|
26-Nov-2006 |
berghofe <none@none> |
Adapted to new nominal_primrec command.
|
#
648c3850 |
|
22-Oct-2006 |
berghofe <none@none> |
Adapted to changes in FCBs.
|
#
6def9b19 |
|
10-Oct-2006 |
urbanc <none@none> |
made some proof look more like the ones in Barendregt
|
#
222f029f |
|
19-Sep-2006 |
urbanc <none@none> |
this file contains a compile-challenge suggested by Adam Chlipala; so far it contains only the definition and no proofs
|