| Wed, 19 Feb 2014 08:34:34 +0100 |
blanchet |
adapted Nitpick to 'primrec' refactoring
|
changeset |
files
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
changeset |
files
|
| Wed, 19 Feb 2014 08:34:32 +0100 |
blanchet |
rewrote a small portion of code to avoid dependency on low-level constant
|
changeset |
files
|
| Wed, 19 Feb 2014 08:33:59 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 19 Feb 2014 17:16:40 +1100 |
kleing |
provide more automation for type definitions (makes book exercises easier)
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:59 +0100 |
blanchet |
prepare two-stage 'primrec' setup
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:58 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:57 +0100 |
blanchet |
removed deadcode
|
changeset |
files
|
| Tue, 18 Feb 2014 23:08:55 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 18 Feb 2014 17:52:28 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 18 Feb 2014 17:52:27 +0100 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
changeset |
files
|
| Tue, 18 Feb 2014 23:03:49 +0100 |
kuncar |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
changeset |
files
|
| Tue, 18 Feb 2014 23:03:47 +0100 |
kuncar |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
changeset |
files
|