| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | tuning | changeset | files |
| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | repaired named derivations | changeset | files |
| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | use the noted theorems in 'BNF_Comp' | changeset | files |
| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | use the noted theorem whenever possible, also in 'BNF_Def' | changeset | files |
| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | use termtab instead of (perhaps overly sensitive) thmtab | changeset | files |
| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms) | changeset | files |