| #
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;
|
| #
48096e82 |
|
03-Dec-2010 |
wenzelm <none@none> |
recoded latin1 as utf8;
use textcomp for some text symbols where it appears appropriate;
|
| #
bf24e024 |
|
15-Dec-2008 |
Christian Urban <urbanc@in.tum.de> |
tuned some proofs
|
| #
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
|
| #
dff24a21 |
|
28-Mar-2008 |
urbanc <none@none> |
tuned proofs
|
| #
56bcf215 |
|
11-Feb-2008 |
urbanc <none@none> |
tuned proofs and comments
|
| #
214105d3 |
|
08-Jan-2008 |
urbanc <none@none> |
tuned proofs
|
| #
84f91899 |
|
04-Jan-2008 |
urbanc <none@none> |
adapted to new inversion rules
|
| #
ffa009b0 |
|
11-Jul-2007 |
berghofe <none@none> |
Renamed inductive2 to inductive.
|
| #
64c652f8 |
|
31-May-2007 |
urbanc <none@none> |
tuned the proof
|
| #
2c991806 |
|
07-May-2007 |
urbanc <none@none> |
polished some proofs
|
| #
9a717367 |
|
03-May-2007 |
urbanc <none@none> |
polished all proofs and made the theory "self-contained"
|
| #
6384e974 |
|
01-May-2007 |
urbanc <none@none> |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
| #
d9dd3c52 |
|
27-Apr-2007 |
urbanc <none@none> |
alternative and much simpler proof for Church-Rosser of Beta-Reduction
|