| Thu, 29 Apr 2010 17:29:53 +0200 | wenzelm | 'write': actually observe the proof structure (like 'let' or 'fix'); | changeset | files |
| Thu, 29 Apr 2010 17:15:23 +0200 | wenzelm | adapted ProofContext.infer_type; | changeset | files |
| Thu, 29 Apr 2010 16:55:22 +0200 | wenzelm | ProofContext.read_const: allow for type constraint (for fixed variable); | changeset | files |