merged

improve "x = A | x = B | x = C"-style fact discovery

transform elim theorems before filtering "bool" and "prop" variables out; another consequence of the transition to FOF

more fiddling with Sledgehammer's "add:" option

beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); another consequence of the transition to FOF

generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"

encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed

fix atomize

improve atomization

fix SInE's error handling + run "vampire" locally if either SPASS or E is missing

added entries

update docs

tuning

parse SNARK proofs

added remote SInE and remote SNARK

no spurious trailing "\n" at the end of Sledgehammer's output

don't get confused by wrong slice

make sure that "add:" doesn't influence the relevance filter too much

tuning of relevance filter

minor cleanup

bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")

update docs

get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"

added "max_relevant_per_iter" option to Sledgehammer

thank Andrei instead of Tanya

fix the relevance filter so that it ignores If, Ex1, Ball, Bex

tuning

reactivated -segprot options, just to make double-sure;

tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input: ML {* fun f x = (x + 1, "aaa") *}

tuned;

tuned signature;

simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);

proper range for hyperlinks and tooltips, using original markup information;

tuned signature;

misc tuning and simplification;

renamed Markup_Tree.Node to Text.Info; Markup_Tree.select: body may depend on full Text.Info, including range; tuned;

removed obsolete Markup_Tree.flatten/filter;

Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;

Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;

tuned signatures;

Command.State: accumulate markup reports uniformly; Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo; tuned;

Markup_Tree.select: misc simplification, proper restriction of parent in subtree;

added Text.Range.- convenience;

tuned signatures;

alternative constructor for Range singularities;

concentrate protocol message formats in Isar_Document;

Branches.overlapping: proper treatment of stop_range that overlaps with end; Markup_Tree.select: allow singularity in parent range specification;

further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;

parameterized type Markup_Tree.Node; Markup_Tree.select: allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;

added toString methods;

misc tuning and simplification;

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;

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);

XML.Cache: pipe-lined (thread-safe) version using actor; tuned Isabelle_Process.pid handling;

simplified internal message format: dropped special Symbol.STX header;

HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);

merged

merged

tuned section on predicate compiler

section "if something goes utterly wrong"

merged

merged

adaptation to new outline

merged

corrected handling of `constrains` elements

removed non-BSD compatible option from cp

Geoff's formatter now needs closed formulas

Using type real does not require a separate logic now.

merged

tuned text about "value" and added note on comments.

simplified command status: interpret stacked markup on demand;

event_bus.scala rather belongs to system plumbing;

some derived operations on Text.Range;

specific types Text.Offset and Text.Range; minor tuning;

moved Text_Edit to Text.Edit; tuned;

moved History/Snapshot to document.scala;

renamed raw_results to raw_protocol;

rename "unit" to "atom", to avoid confusion with the unit type;

document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;

use Synchronized.var and prevent global CRITICAL sections in this hot spot;

renamed create_id to new_id;

more explicit / functional ML version of document model; tuned;

renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;

fixed Isabelle/Scala build (cf. f3220ef79d51);

Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;

more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;

Keyword.status: always suppress position;

moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;

merged

robustified proof

lemma execute_bind_case

unit and bool are instances of heap

merged

sketch of new outline

sketch of new outline

ditem

refined abstract

added stub "If something utterly fails"

avoid variable name acc (cf. cs. 3142c1e21a0e)

import swap prevents strange failure of SML code generator for datatypes

added setup

merged

group record-related ML files

merged

dropped dead code

moved Record.thy from session Plain to Main; avoid variable name acc

group record-related ML files

Class.declare -> Class.const

named target is optional; explicit Name_Target.reinit

named target is optional

Named_Target.init: empty string represents theory target

Named_Target.theory_init

simplified code

tuned

tuned

merged

tuned whitespace

tuned internal structure

remove reinit operation alltogether

avoid arcane Local_Theory.reinit entirely

more convenient split of class modules: class and class_declaration

tuned

stripped signature

explicit accessed to structure Class_Target

tuned lowercase

moved Document.text_edits to Thy_Syntax;

tuned;