| #
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;
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
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.
|
| #
69dacf0c |
|
12-Jun-2008 |
urbanc <none@none> |
emoved the parts that deal with the CK machine to a new theory
|
| #
2932189d |
|
22-May-2008 |
urbanc <none@none> |
made the naming of the induction principles consistent: weak_induct is
induct and induct is strong_induct
|
| #
ccdbc453 |
|
16-May-2008 |
urbanc <none@none> |
added a lemma about existence of contexts
|
| #
50288858 |
|
01-May-2008 |
urbanc <none@none> |
tuned some proofs and comments
|
| #
214105d3 |
|
08-Jan-2008 |
urbanc <none@none> |
tuned proofs
|
| #
6c045ad1 |
|
06-Jan-2008 |
urbanc <none@none> |
some pre-release tunings
|
| #
5a64f8c1 |
|
31-Dec-2007 |
urbanc <none@none> |
tuned proofs and comments
|
| #
28e1a742 |
|
19-Dec-2007 |
urbanc <none@none> |
polishing of some proofs
|
| #
3381a631 |
|
28-Nov-2007 |
urbanc <none@none> |
an example file for how to treat Felleisen-Hieb-style contexts
in nominal
|