| Thu, 17 Apr 2008 22:22:25 +0200 | wenzelm | prove_global: Variable.set_body true, pass context; | changeset | files |
| Thu, 17 Apr 2008 22:22:23 +0200 | wenzelm | adapted to ProofContext.revert_skolem: extra Name.clean required; | changeset | files |
| Thu, 17 Apr 2008 22:22:21 +0200 | wenzelm | prove_global: pass context; | changeset | files |
| Thu, 17 Apr 2008 22:22:19 +0200 | wenzelm | pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest); | changeset | files |
| Thu, 17 Apr 2008 16:30:55 +0200 | wenzelm | replaced token translations by common markup; | changeset | files |
| Thu, 17 Apr 2008 16:30:53 +0200 | wenzelm | moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output; | changeset | files |
| Thu, 17 Apr 2008 16:30:52 +0200 | wenzelm | token translations: context dependent, result Pretty.T; | changeset | files |