| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | stick to external proofs when invoking E, because they are more detailed and do not merge steps | changeset | files |
| Thu, 24 Jul 2014 00:24:00 +0200 | blanchet | more robust handling of types for skolems (modeled as Frees) | changeset | files |
| 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 |