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;

added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);

do not buffer fifo streams here -- done in Isabelle_Process; removed misleading comments -- blocking on open is not reliable on non-standard systems (Cygwin);

explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;

edit_document: more precise status position;

added get_after convenience;

more basic notion of unparsed input;

simplified/clarified Change: transition prev --edits--> result, based on futures; Session.history: plain List instead of somewhat indirect Change.ancestors; tuned;

moved snapshot to Session (cf. 96b22dfeb56a);

Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway; Document.edit_text: create new document id here;

clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;

misc tuning and simplification;

specific command state;

specific Session.Commands_Changed;

consider snapshot as service of Session, not Document.Change;

tuned scope;

Document.print_id;

consider command state as part of Snapshot, not Document;

represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);

Named_Target;

modernized specifications; tuned headers;

spelling;

merged

renamed Theory_Target to the more appropriate Named_Target

discontinue old implementation of `foundation`

moved instantiation target formally to class_target.ML

NEWS

merged

print fcomp combinator only monadic in connection with other monadic expressions

merged

merged

moved overloading target formally to overloading.ML

moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order

merged

whitespace tuning

remove overloading and instantiation from data slot

removed obsolete Toplevel.enter_proof_body;

standardized pretty printing of consts (e.g. see find_theorems, print_theory);

misc tuning and simplification;

simplified/unified command setup;

removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);

prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining; tuned;

prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;

tuned eval_thms (cf. note etc. in proof.ML);

use Pretty.enum convenience;

tuned whitespace;

more precise and more maintainable dependencies;

merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;

* -> prod

added .ML extension

avoid old unnamed infix

avoid inclusion of Natural module in generated code

explicit ML extension

merged

separate initialisation for overloading and instantiation target

different foundations for different targets; simplified syntax handling of abbreviations

deleted duplicate lemma

Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.

basic renumbering

avoiding redundant primes

separated type from term parameters

moved extra_tfrees check for mixfix syntax to Generic_Target

name and argument grouping tuning

whitespace tuning

added generic_target.ML

try to uniformly follow define/note/abbrev/declaration order as close as possible

split off structure Generic_Target into separate file

split off generic parts of target implementations into separate structure

restructured code for `declaration`

executable relation operations contributed by Tjark Weber

factored out foundation of `define` into separate function

combine declaration and definition of foundation constant

more appropriate outline of `define`

backlink definition to target `notes`

merged

dropped idle local_facts argument; factored out theory_abbrev and locale_abbrev

more convenient order

dropped misleading comments

merged

separated foundation of `notes`

more clear separation into local and global facts

sharpened and tuned educated guess for canonical class morphism

minimize sorts in certificate instantiation

prevent ATP thread for staying around for 1 minute if an exception occurred earlier; this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch

adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present

"declare" -> "declaration" (typo)

replace "setup" with "declaration"

disable Nitpick on Cygwin while I'm on vacation; I'll look into the timeout once I'm back

merged

use "declaration" instead of "setup" to register Nitpick extensions

remove needless "open"

move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)

fiddle some more with "max_new_relevant_facts_per_iter"

replace recursion with "fold"

remove debugging output

remove now needless "Thm.transfer"

reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF

merge

fix embarrassing bug in elim rule handling, introduced during the port to FOF

minor doc changes

modernized some specifications;

tuned;

Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;

native Isabelle_Process commands, based on efficient byte channel protocol for string lists; misc clarification of proc/pid state, eliminated closing flag; misc tuning and simplification;

proper handling of empty text; more informative exceptions;

more uniform XML/YXML string_of_body/string_of_tree;

type XML.Body as basic data representation language (Scala version); tuned;

type XML.body as basic data representation language; tuned;

renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;

added string_bytes convenience;

tuned;

removed obsolete methods for (ML) commands;

prefer Nimbus look and feel on all platforms, instead of the somewhat ugly javax.swing.plaf.metal.MetalLookAndFeel, which presumably is implicit fall-back nonetheless;

edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;

distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names; asynchronous Isabelle_Process.init -- raw ML toplevel stays active; simplified Isabelle_Process using actors; misc tuning;

added Library.thread_actor -- thread as actor;

clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES; static default Dactors.corePoolSize=4 for more reproducible concurrency, independently of number of cores;

auto_flush: higher frequency;

uniform raw_dump for input/output fifos on Cygwin;

more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;

Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin;

tuned comments;

merged

added Lars Noschinski to isatest report

merged

discontinued separation of `define` and `declare_const`

unravelled target initialization code

added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)

added scanning of if-then-else expressions

merged

added support for partial quotient types; previously Nitpick was unsound for these

adapt occurrences of renamed Nitpick functions

document the non-legacy interfaces

local versions of Nitpick.register_xxx functions

parse_spans: somewhat faster low-level implementation;

proper context for Syntax.parse_token;

prefer Context_Position.report where a proper context is available -- notably for "inner" entities;

explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);

fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;

YXML.parse: refrain from interning, let XML.Cache do it (partially);

cache_string: store trimmed string value;

simple_dialog: allow scala.swing.Component as well;

simplified some Markup;

simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added Isabelle_Process.Result.properties;

more robust treatment of Markup.token;

simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;

concentrate structural document notions in document.scala; tuned;

maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);

tuned;

more explicit model of pending text edits;

more explicit treatment of Swing thread context; Document_Model.snapshot: require Swing thread;

replaced individual Document_Model history by all-inclusive one in Session; Document_Model: provide thy_name externally, i.e. by central Isabelle plugin; tuned;

misc tuning and clarification;

avoid null in Scala; tuned comments;

updated keywords;

removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);

merged

merged

quotient types registered as codatatypes are no longer quotient types

added a friendly warning

extend the scope of limitation about nonconservative extensions

improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"

Remove duplicate locale activation code; performance improvement.

added record field

added "whack"

handle "Rep_unit" & Co. gracefully

added support for "Abs_" and "Rep_" functions on quotient types

fiddle with specialization etc.

handle inductive predicates correctly after change in "def" semantics

don't specialize built-ins or constructors

more docs

prevent the expansion of too large definitions -- use equations for these instead

make nitpick accept "==" for "nitpick_(p)simp"s

fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization

deal correctly with Pure.conjunction in mono check

rename internal functions

remove buggy and needless condition

renamed internal function

Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities

avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)

improve datatype symmetry breaking; all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example

merged

make SML/NJ happy

get rid of all "optimizations" regarding "unit" and other cardinality-1 types

tuning

better "Pretty" handling

change formula for enumerating scopes

example tweaking -- also prevents Nitpick_Tests from using more than 1 thread

speed up Nitpick examples a little bit

minor changes

updated example timings

more helpful message

also mention gfp

bump up the max cardinalities, to use up more of the time given to us by the user

make tracing monotonicity easier

more documentation, based on email discussions with a user

make example easier to parse

clarify attribute documentation

choose better example

fix newly introduced bug w.r.t. conditional equations

document something I explained in an email to a poweruser

make Nitpick more flexible when parsing (p)simp rules

fix soundness bug w.r.t. "Suc" with "binary_ints"

handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld

optimize local "def"s by treating them as definitions

careful about which linear inductive predicates should be starred

help Nitpick

fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors

prevent generation of needless specialized constants etc.

optimize generated Kodkod formula

prefer implication to equality, to be more SAT solver friendly

minor symmetry breaking for codatatypes like llist

fix bug with mutually recursive and nested codatatypes

fix minor bug in sym breaking

modernized specifications; tuned headers;

Document_Model: include token marker here;

tuned;

misc tuning -- produce reverse_edits at most once (note that foldRight produces a reversed list internally, while recursion is infisible due to small stack vs. large stack frames on JVM);

editor mode;

Text_Edit.convert/revert;

renamed to_current to convert, and from_current to revert;

Change.Snapshot: include from_current/to_current here, with precomputed changes;

explicit Change.Snapshot and Document.Node; misc tuning and clarification; Document_View: explicitly highlight outdated command status;

simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;

somewhat uniform Thy_Header.split_thy_path in ML and Scala;

uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);

load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;

export use_thys_wrt;

more precise CRITICAL sections, using NAMED_CRITICAL uniformly;

updated to Netbeans 6.9;

schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;

more precise CRITICAL sections; tuned;

removed unused Update_Time data (cf. ac94ff28e9e1);

modernized specifications; tuned headers;

eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;

find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);

renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);

tuned headers -- more precise load path;

theory loading: only the master source file is looked-up in the implicit load path;

load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;

simplified/clarified Thy_Load path: search for master only, lookup other files relative to that; tuned;

only test prolog code examples if environment variable is set

Revised proof of long division contributed by Jesus Aransay.

fix bug with Kodkodi < 1.2.14

merged

document new Nitpick options

tweak datatype sym break code

added manual symmetry breaking for datatypes

change the order of the SAT solvers, from fastest to slowest

started implementation of custom sym break

clarify Nitpick's output in case of a potential counterexample

added support for CryptoMiniSat

gracefully handle the case where no integers occur in the formula and the "max" option is used

merged

adding Code_Prolog theory to IsaMakefile and HOL-Library root file

inductive_simps learns to have more tool compliance

setting up Code_Prolog_Examples

adding queens and symbolic derivation example for prolog code generation

adding parsing of numbers; improving output of solution without free variables in prolog code generation

adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation

adding basic arithmetic support for prolog code generation

adding numbers as basic term in prolog code generation

More consistent naming of locale api functions.

Documentation of 'interpret' updated.

print_interps shows interpretations in proofs.

Interpretation in proofs supports mixins.

Make registrations generic data.

merged

don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

fix Mirabelle timeout

make Mirabelle happy

fix bug in the newly introduced "bound concealing" code

handle division by zero gracefully (used to raise Unordered later on)

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses

fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)

handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

revert exception throwing in FOL_SOLVE, since they're not caught anyway

avoid "ATP Error: Error: blah" style messages

avoid "_def_raw" theorems

better error and minimizer output

deal with chained facts more gracefully

speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"

work around atomization failures

fiddle with the fudge factors, to get similar results as before

perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs

fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)

generate correct names for "$true" and "$false"; this was lost somewhere in the non-clausification

don't assume canonical rule format

avoid "clause" and "cnf" terminology where it no longer makes sense

"axiom_clauses" -> "axioms" (these are no longer clauses)

remove the "extra_clauses" business introduced in 19a5f1c8a844; it isn't working reliably because of: * relevance_override * it is ignored anyway by TPTP generator A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable

adapting output for first solution

removing pointless type information in internal prolog terms

cleaning example file; more natural ordering of variable names

improving translation to prolog; restoring terms from prolog output; adding tracing support

working on parser for prolog reponse

querying for multiple solutions in values command for prolog execution

correcting scanning

adding values command and parsing prolog output

adding example file for prolog code generation; adding prolog code generation example to IsaMakefile

adding a mockup version for prolog code generation

exporting retrieval function for graph of introduction rules in the predicate compiler core

merged

rebinding ref is illegal

tuned example

intermediate operation avoids invariance problem in Scala

merged

kill polymorphic "val"s

improved ATP error handling some more

shorter URL

mention version numbers

fiddled with usage text

handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on

merged

tuned printing of applications and let cascades

checking Scala_imp

proper unit type in transformed program

merged

merged

tuned; added pretty numerals for code generation

may use `int` in Isabelle runtime environment

dropped dead code

merged

make Mirabelle happy

renamed environment variable

updated component name

consequence of directory renaming

rename directory

minor refactoring

minor refactoring

updated Sledgehammer docs

remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway

remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts

fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses

revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well; we can no longer just count the formulas, because for some reason E's numbering either no longer starts at 1 or it doesn't increment by 1 at each step

more robust proof reconstruction

adapt to new (?) TPTP output

fix remote_vampire's proof reconstruction

fix proof reconstruction for latest Vampire

renaming

support latest version of Vampire (1.0) locally

improve detection of installed SPASS