wenzelm [Fri, 18 Apr 2008 23:49:40 +0200] rev 26720
modernized specifications and proofs;
haftmann [Fri, 18 Apr 2008 09:44:16 +0200] rev 26719
improved definition of upd
wenzelm [Thu, 17 Apr 2008 22:28:56 +0200] rev 26718
* Context-dependent token translations.
wenzelm [Thu, 17 Apr 2008 22:22:30 +0200] rev 26717
revert_skolem: do not change non-reversible names;
default token translations: revert_skolem;
removed obsolete revert_skolems;
wenzelm [Thu, 17 Apr 2008 22:22:28 +0200] rev 26716
print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm [Thu, 17 Apr 2008 22:22:27 +0200] rev 26715
no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
wenzelm [Thu, 17 Apr 2008 22:22:26 +0200] rev 26714
variant_fixes: preserve internal state, mark skolem only for body mode;
import_inst: actually observe is_open flag (cf. variant_fixes);
wenzelm [Thu, 17 Apr 2008 22:22:25 +0200] rev 26713
prove_global: Variable.set_body true, pass context;
wenzelm [Thu, 17 Apr 2008 22:22:23 +0200] rev 26712
adapted to ProofContext.revert_skolem: extra Name.clean required;
wenzelm [Thu, 17 Apr 2008 22:22:21 +0200] rev 26711
prove_global: pass context;