wenzelm [Fri, 18 Apr 2008 23:49:46 +0200] rev 26722
print_cases: proper context for revert_skolem;
wenzelm [Fri, 18 Apr 2008 23:49:44 +0200] rev 26721
tuned;
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;