| #
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;
|
| #
7a4b6a89 |
|
21-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
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.
|
| #
65b87b21 |
|
28-Aug-2008 |
krauss <none@none> |
more function -> fun
|
| #
2932189d |
|
22-May-2008 |
urbanc <none@none> |
made the naming of the induction principles consistent: weak_induct is
induct and induct is strong_induct
|
| #
214105d3 |
|
08-Jan-2008 |
urbanc <none@none> |
tuned proofs
|
| #
a62c3c6d |
|
12-Aug-2007 |
wenzelm <none@none> |
added type constraints to resolve syntax ambiguities;
|
| #
ffa009b0 |
|
11-Jul-2007 |
berghofe <none@none> |
Renamed inductive2 to inductive.
|
| #
b57d2603 |
|
21-Jun-2007 |
wenzelm <none@none> |
tuned proofs -- avoid implicit prems;
|
| #
8dcc70e7 |
|
11-Jun-2007 |
chaieb <none@none> |
tuned Proof
|
| #
6b48a73e |
|
04-Jun-2007 |
urbanc <none@none> |
added a few comments to the proofs
|
| #
b7a2a5ae |
|
31-May-2007 |
urbanc <none@none> |
a theory using locally nameless terms and strong induction principles
|