| 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 |
| Thu, 29 Apr 2010 16:53:08 +0200 | wenzelm | avoid clash with keyword 'write'; | changeset | files |
| Thu, 29 Apr 2010 11:05:13 +0200 | wenzelm | allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax; | changeset | files |
| Thu, 29 Apr 2010 11:00:32 +0200 | wenzelm | uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b); | changeset | files |