stub for evaluation chapter

updated generated document

dropped errorneous underscore

output whitespace tuning

use command_def

use command_def vs. command more consciously

removed Code_Prolog: modifies global environment setup non-conservatively

pretty constraint syntax; tuned theory imports

added quick and dirty section on invariants

base on HOL-Library

more antiquotations

deglobalization

Tuned.

merged

repair translation of "c_fequal"

tweaking

merged

enforcing a singleton type inference parameter after type inference and before fixation prevents multiple type variables in import during class declaration

merged

invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms; this resulted in a subtle soundness bug in Sledgehammer -- introduced by the transition to FOF

tuning

more parentheses in TPTP formulas, just in case

handle E's Skolem constants more gracefully

improve detection of old Vampire versions

Markup_Tree.select: crude version of stream-based filtering;

Text.Range: improved handling of singularities;

tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;

moved Isar_Document to Pure/PIDE;