prefer ML_file over old uses;

prefer ML_file over old uses;

'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';

add keywords of this node as well (e.g. relevant for Pure.thy);

tuned;

tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;

discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;

find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;

clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;

pass syntax through check_thy;

use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;

clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;

tuned;

clarified bootstrapping of Pure;

tuned errors;

prefer File.full_path in accordance to check_file;

more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

updated Thy_Load.check_thy;

refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;

more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;

some support for thy_load_commands; clarified signatures;

tuned signature;

clarified initialization of Thy_Load, Thy_Info, Session;

tuned;

more robust cleaning of "% tag" and "-- cmt";

some support for inlining file content into outer syntax token language;

tuned comment;

tuned;

added keyword kind "thy_load" (with optional list of file extensions);

updated generated files;

more strict syntax, according to manual;

abstracted lemma

retain unknown options within preferences; tuned print;

more comprehensible platform family name;

tuned message;

fewer components, more roots;

actually remove makeall (cf. 292b97e17fb7);

tuned;

Backed out changeset ec82c33c75f8;

Typo fixed.

merged

merged

fixed lemmas

abstracted lemmas

updated to new init_components, hoping that mira can digest that;

some explanations on component categories;

specific cygwin components;

obsolete;

some explanations on isabelle components;

some grouping of components;

renamed components to components_old, to make room for some directory of the same name;

minor robustification;

added "isabelle components" tool;

tuned;

direct support for component forests via init_components; explicit ISABELLE_COMPONENTS_MISSING;

allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira; clarified spaces in file names -- ISABELLE_HOME is non-critical after abolishment of "make";

tuned;

tuned;

updated component repository;

updates on 32 bit vs. 64 bit platforms; added Mountain Lion; dropped Leopard; tuned;

updated to jedit_build-20120813, pointing to another contrib directory as a change;

merged

tuned proofs;

look in current directory first before looking up includes in the TPTP directory, as required by Geoff

prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala

more robust multi-platform support;

updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;

support for jdk-7u6 component;

Clarification: free variables allowed in interpreted locale instances.

merged

fixed proof

abstracted lemmas

Backed out changeset 6cf7a9d8bbaf

abstracted lemmas

merged

Turned into Admin tool download_components.

tuned;

tuned;

some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");

tuned;

fixed handling of "int" in the wake of its port to the quotient package

removed dead code

merged

Added various options, notably -c to download components listed in Admin/components. Also, curl instead of wget.

ignore some administrative files on newer Mercurial versions as well;

some support for persistent user preferences;

merged

explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;

more direct interpretation of document_variants for build (unchanged for usedir);

tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0

fixed then-else confusion

tweak Vampire setup in the light of new evaluation

improved set of reconstructor methods

warn users about unused "using" facts

be less aggressive at kicking out chained facts

recognize bus errors as crash

consider removing chained facts last, so that they're more likely to be kept

clarified format of etc/options: only declarations, not re-definitions;

check_errors for cumulative session content;

even more defensive path expansion (see also 8d381fdef898);

support for 'typ' with explicit sort constraint;

added jedit option -d;

always retain doc-src (as regular component);

merged

Calling isabelle with proper (relative) path, no longer relying on $PATH.

fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;

updated to jedit-4.5.2 (still unchanged);

restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself

tuned;

fixed mira.py (cf. fd50596bf78b)

more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;

more static antiquotations;

always show some timing information, to reduce the need for explicit -v;

some information for central Isabelle repository configuration;

reduced settings patching

removed obsolete configuration AFP_images

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

simplified symbol matching;

further clarification of malformed symbols;

more liberal scanning of potentially malformed symbols;

vacuous execution after first malformed command;

clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;

tuned markup;

tuned message;

clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);

reports with body text, not just markup;

fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end

special code with lists no longer necessary, use sets

proper error prefixes;

more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;

tuned message;

clarified Linear_Set.next/prev: check definedness;

merged

Improved complete lattice formalisation - no more index set.

merged

tuned proofs;

sneak message into "bad" markup as property -- to be displayed after YXML parsing;

apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;

clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;

tuned;

discontinued mostly unused markup for command spans;

more visible markup of malformed input as "bad";

tuned proofs

some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;

refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.; tuned signature;

tuned signature;

more direct Linear_Set.reverse, swapping orientation of the graph; tuned;

tuned signature;

tuned;

refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;

explicit FIXME;

tuned signature;

corrected header

refined isabelle mkroot; allow empty 'theories' to facilitate generated templates;

simplified session specifications: names are taken verbatim and current directory is default;

added build option -D: include session directory and select its sessions;

discontinued obsolete "isabelle makeall";

even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);

back to implicit commit via isabelle-process -- save image only once (cf. 181b91e1d1c1);

proper axiomatization of "mem" -- do not leave it formally unspecified;

simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;

more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;

obsolete;

eliminated obsolete ISABELLE_USEDIR_OPTIONS;

updated ML settings;

add legacy target for HOL-Probability, needed by AFP/Markov_Models

proper isabelle update_keywords tool;

configure Admin as component, with its own lib/Tools;

SOMEthing went utterly wrong in 5b51ccdc8623;

more legacy targets;

discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;

tuned;

proper quoting

merged

more structural parsing for minor modes; tuned signatures;

clarified Sidekick configuration, including minor modes;

stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users

specify full path to clausifier

documentation

more token markers, based on actual outer syntax; prefer official Outer_Syntax.init with its completions;

simplified process startup phases: INIT suffices for is_ready;

need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";

prefer static Build.session_content for loaded theories -- discontinued incremental protocol;

prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;

permissive outer syntax wrt. symbol recoding;

simplified Document.Node.Header -- internalized errors;

tuned signature;

tuned signature -- slightly more abstract text representation of prover process;

tuned signature -- make Pretty less dependent on Symbol;

extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)

increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)

documentation

added iProver(-Eq) local

optimized saving

pass Isabelle/Scala system options into ML process of Isar tty or build jobs;

merged

switching from Emacs.app to Aquamacs.app

switching from Emacs.app to Aquamacs.app

modify group_cancel simprocs so that they can cancel multiple terms at once

"isabelle options" prints Isabelle system options;

removed leftover from 89cc3dfb383b, hoping that mira digests it;

discontinued presumably obsolete attempts at doc-src testing (cf. 3b02b0ef8d48, 89cc3dfb383b);

more precise imitation of old ROOT.ML files;

fixed mira.py (cf. fe611991427a)

corrected session name

removed obsolete mira configurations -- covered by AFP_images

modernized mira configurations, making use of isabelle build

removed mira configurations related to old importer

re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;

more on isabelle mkroot;

added mkroot: prepare session root directory;

prefer general Command_Line.tool wrapper (cf. Scala version);

simplified Session_Tree; tuned messages;

some timeouts, which modify the build order;

queue ordering by descending outdegree and timeout;

tuned import;

clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);

clarified Session_Entry vs. Session_Info with related parsing operations; more error positions;

simplified class Job; tuned message;

let with_timing report overall number of threads;

further robustification of interrupts during build;

refined outer syntax;

prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);

remember ATP flops to avoid repeating them too quickly

remember which MaSh proofs were found using ATPs

rule out same "technical" theories for MePo as for MaSh

don't generate queries for empty dependencies

crank up max number of dependencies

never use MaSh in Metis examples, to avoid one dimension of nondeterminism

merged

more informative process exit code;

timeout for session build job; tuned error messages;

static outer syntax based on session specifications;

declare trE and tr_induct as default cases and induct rules for type tr

reject path variable nesting explicitly;

simplified custom document/build script, instead of old-style document/IsaMakefile;

cleaner temporary file cleanup for MaSh, based on tried-and-trusted code

merged

don't tag negatively naked variables

support older versions of Vampire

document E-MaLeS

added E-MaLeS to list of provers for testing

discontinued unused etc/sessions catalog;

allow session specifications in arbitrary order;

tuned;

report commands as formal entities, with def/ref positions;

more official command specifications, including source position;

more antiquotations;

declare keywords only once;

more antiquotations;

more antiquotations;

more standard bootstrapping of Pure outer syntax;

fixed document;

store parent heap stamp as well -- needs to be propagated through the build hierarchy; misc tuning;

more standard bootstrapping of Pure.thy;

more precise guide for bibtex/makeindex -- dummy files should be sufficient;

added offline test for skip_proofs;

clarified ISABELLE_FULL_TEST;

explicit option skip_proofs;

recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);

removed junk;

no longer force STIX fonts onto the user -- NB: STIXv1.0.0 is outdated and Mac OS 10.7 ships its own copy of STIX already;

more prominent file name;

updated isatest settings for isabelle build;

more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;

merged

print full path;

Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now

add testing file for RBT_Set

implementation of sets by RBT trees for the code generator

use lifting/transfer formalization of RBT from Lift_RBT

a couple of additions to RBT formalization to allow us to implement RBT_Set

more relation operations expressed by Finite_Set.fold

more set operations expressed by Finite_Set.fold

moved another larger quickcheck example to Quickcheck_Benchmark

HOL-Probability appears to work with smlnj;

document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;

made SML/NJ happy;

renamed session TLA to HOL-TLA to avoid clash with AFP;

clarified directory content operations (similar to ML version);

regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);

multi-threaded HOL-Tutorial with explicit indication of local options;

removed obsolete IsaMakefile + ROOT.ML setup -- doc-src is managed via isabelle build;

removed some old material (inactive since 2002/2003);

updated isatest to isabelle build, which also includes doc-src sessions;

obsolete;

makedist -D retains doc-src component with its "doc" sessions (relevant for testing);

allow negative int values as well, according to real = int | float;

misc tuning;

discontinued unused isabelle jedit debugger; tuned;

more uniform usage of "isabelle tool";

less verbosity;

proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;

tuned signature;

updated ROOT according to 3defa60a7ae3;

merged

re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples

added build option -c; tuned;

removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;

script for downloading components from central store

added build option -f;

corrected slip

discontinued $ISABELLE_HOME/build (cf. 500c6eb6c6dc);

separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;

added Quickcheck_Benchmark (cf. 1959baa22632);

no apparent need for single-threaded execution;

discontinued obsolete Isabelle/build script;

announce advanced support for Isabelle sessions and build management;

some introduction on sessions;

tuned messages;

tuned;

added generated file;

some description of main build options;

more on "Session ROOT specifications";

some description of isabelle build;

tuned;

isabelle browser is another user interface;

renamed isabelle-root minor mode;

discontinued special treatment of Proof General;

top-down order of user interfaces;

misc tuning;

move exception handlers outside of let block

tuned message;

merged

evaluation: allow multiple code modules

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

merged

restored narrowing quickcheck after 6efff142bb54

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;

tuned proofs -- avoid odd situations of polymorphic Frees in goal state;

move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used

replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms

give Nat_Arith simprocs proper name bindings by using simproc_setup

tweaks in preparation for type encoding evaluation

merged

replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones

nicer Nitpick subscript output in jEdit

no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;

proper shell variable;

actually check return code;

include doc-src as component, and thus its sessions defined in ROOT;

tuned signature;

delete other log file;

simplified Path vs. JVM File operations;

tuned;

tuned messages;

fewer options;

tuned signature;

prefer explicit datatype Present.dump_mode;

simplified Session.name;

more precise imitation of usedir wrt. Session.name (cf. 45137257399a);

update docs

extract Z3 unsat cores (for "z3_tptp")

bring implementation of traditional encoding in line with paper

further refinement of current/all_current status, which needs to be propagated through the hierarchy (see also Thy_Info.require_thys);

merged

[1] goes after any attributes

Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here

detect unknown options again

Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)

don't export technical theorems for MaSh

repaired accessibility chains generated by MaSh exporter + tuned one function out

generate fact name in queries again + use ATP dependencies when possible

proper all_current, which regards parent status as well;

more build options;

added session HOL-Tutorial;

recovered chapter on Presenting Theories;

avoid clash of Misc/pairs.thy and Types/Pairs.thy on case-insensible file-system;

proper input;

recovered latex job;

adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets;

more build options;

simplified Tutorial sessions; moved original version of generated .tex sources;

proper arguments for old usedir;

more precise imports;

refined "document_dump_mode": "all", "tex+sty", "tex";

allow spaces in file names;

more files for session Pure;

discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;

tuned;

remove old output heaps, to ensure that result is valid wrt. check_stamps; tuned signature;

proper imports;

support session groups; tuned signature;

discontinued slightly odd session order, which did not quite work out;

tuned signature;

avoid clash of Advanced/simp.thy vs. Misc/simp.thy;

tuned signature;

actually check source vs. target stamps, based on information from log files;

tuned;

session specifications for doc-src, excluding TutorialI for now;

updated generated files;

clarified no_document situation;

no hardwired default for Proof General component -- its users can use init_component separately;

rail no longer exists;

some updates on "Building a repository version of Isabelle";

added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;

more standard session setup for WWW_Find;

read/write dependency information; tuned signature;

more files;

more build options;

merged

moving a first Quickcheck example with many computations into a separate session Quickcheck_Benchmark

moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure

reactivated HOL-NSA-Examples;

tuned order;

more build options;

tuned error;

more explicit checks during parsing;

more explicit document = false to reduce warnings; tuned;

pass parent_base_name, which is required for Session.init sanity check; tuned message;

more session entries;

modernized imports;

more general notion of user ERROR (cf. 44f56fe01528);

tuned messages;

tuned message;

human-readable I/O error;

more session ROOT files;

tuned messages (cf. isabelle makeall);

tuned message;

actually negate "document" (cf. 7483aa690b4f);

clarified no_build vs. verbose;

clarified "document" again, eliminated redundant "no_document";

clarified build -n (no build);

added "document_dump_only" (cf. negated usedir -C);

more precise propagation of options: build, session, theories;

further imitation of ISABELLE_USEDIR_OPTIONS via options;

observe "condition";

observe "quick_and_dirty";

added "browser_info_remote" (cf. usedir -P);

clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;

timing for whole session;

tuned options;

timing is command line options, not system option;

clarified document options;

pass build options to ML; some imitation of usedir Session.init;

added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);

provide explicit ISABELLE_PLATFORM32 as well; discontinued some obsolete platforms; explicit error for unknown platform;

merged

set_vcs now derives prefix from fully qualified procedure / function name

try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);

updated to Platypus 4.7;

merged

tuned;

clarified init_component: always liberal; reduced divergence of clone from lib/scripts/getsettings;

added system build mode: produce output in ISABELLE_HOME; determine output location more explicitly;

removed redundant check (cf. a8ed41b6280b);

pass ISABELLE_BROWSER_INFO as explicit argument;

removed some old/unused stuff;

updated smlnj settings;

cap the number of facts returned by MaSh

remove MaSh junk associated with size functions

identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway

removed MaSh junk arising from primrec definitions

distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh

tuning

faster "save" operation

include unknown local facts in MaSh

ensure all calls to "mash" program are synchronous

don't relearn old facts in Isar mode

took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks

restrict unqualified imports from Haskell Prelude to a small set of fundamental operations

more correct import

merged

NEWS

library theories for debugging and parallel computing using code generation towards Isabelle/ML

also consider current working directory (cf. 3a5a5a992519)

parallel scheduling of jobs; misc tuning;

tuned;

maintain set of source digests, including relevant parts of session entry;

determine source dependencies, relatively to preloaded theories; tuned signature;

propagate defined options; misc tuning;

disallow quotes in path specifications -- extra paranoia;

save image for inner nodes only; misc tuning and simplification;

some actual build function on ML side; further imitation of "usedir" shell script;

tuned -- no dependency on exit function;

more ML_System operations;

restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs

handling partiality in the case where the equality optimisation is applied

merged