updated some isatest settings;

added generated file;

merged

tuned quotes

more antiquotations

deglobalized named HOL constants

deglobalized named HOL constants

corrected some long-overseen misperceptions in recdef

use HOLogic.boolT and @{typ bool} more pervasively

tuned

some more antiquotations

tuned

use antiquotations for remaining unqualified constants in HOL

tuned

tuned declaration order

merged

NEWS

re-added instantiation of type class random for records

tuned signature and code

adjusted to restored naming convention of logical record types

robustified proof

adjusted to changed naming convention of logical record types

removed separate quickcheck_record module

liberal instantiation of class eq; tuned naming scheme

more helpful NEWS entry

dropped SML typedef_codegen: does not fit to code equations for record operations any longer

preemptive NEWS

tuned code

use extension constant as formal constructor of logical record type

deleted typecopy package

authentic syntax allows simplification of type names

dropped make_/dest_ naming convention

formally integrated typecopy layer into record package

eliminated typecopy interpretation

moved spurious auxiliary lemma here

tuned proof

qualified constants Let and If

NEWS

merged

deglobalization

merged

merged

rename enum values

handle bound name conflicts gracefully in FOF translation

with Kodkodi 1.2.15, Java 1.5 is fine

gracefully handle the case where the JVM is too old in Nitpick

improve SPASS clause numbering hack

deglobalization

more antiquotations

added equality instantiation

use command_def more consciously

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;

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;