| Thu, 29 Apr 2010 17:47:53 +0200 | wenzelm | allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command; | changeset | files |
| 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 |