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;

tuned Markup_Tree, using SortedMap more carefully;

Output_Position.report_text -- markup with potential "arguments";

Command.status: full XML.Tree, i.e. Markup with potential "arguments";

more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;

tuned;

refined notion of Text.Range;

decode Isabelle symbol positions in one spot;

tuned;

uniform Markup.empty/Markup.Empty in ML and Scala;

digesting strings according to SHA-1 -- Scala version;

pro-forma support for further platforms;

report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;

discontinued support for Poly/ML 5.0 and 5.1 versions;

updated for prospective Poly/ML 5.4;

multi-platform build script for Poly/ML;

updated keywords;

updated Named_Target.init;

made 9043eefe8d71 actually compile;

merged

merged

formally document `code abstype` and `code abstract` attributes

NEWS and CONTRIBUTORS

nicer code for rev

reworked section on simple datatype refinement

tuned whitespace

merged

typos in comment

more debug output

detect old Vampire and give a nicer error message

merged

now works for schematic terms as well, thanks to Alex for the `how-to'

added section on program refinement

tuned whitespace

tune;

added functor Linear_Set, based on former adhoc structures in document.ML; Linear_Set.delete_after (ML): actually delete table entries; Scala Linear_Set: clarified exceptions, according to ML version; simplified Document.node using Linear_Set; ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;

HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);