| Thu, 15 Aug 2019 21:18:06 +0200 | wenzelm | more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration; | changeset | files |
| Thu, 15 Aug 2019 19:35:17 +0200 | wenzelm | more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof; | changeset | files |
| Thu, 15 Aug 2019 18:21:12 +0200 | wenzelm | support Export_Theory.read_proof, based on theory_name and serial; | changeset | files |
| Thu, 15 Aug 2019 16:57:09 +0200 | wenzelm | clarified PThm: theory_name simplifies retrieval from exports; | changeset | files |