discontinued old ISABELLE and ISATOOL environment settings;

shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;

removed further remains of mutable theory data (cf. 25bd3ed2ac9f);

merged

code cache only persists on equal theories

moved name duplicates to end of theory; reduced warning noise

merged

modernized

added applify combinator

dropped redundant name declarations

dropped copy operation for legacy TheoryDataFun

code cache without copy; tuned

report keywords as singleton messages, control message kind via print mode;

explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);

omit useless (?) scaladoc;

added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;

after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;

discontinued special HOL_USEDIR_OPTIONS;

updated stats;

made SML/NJ happy;

merged

removed legacy asm_lr_simp_tac

removed more asm_rl's - unfortunately slowdown of 1 min.

new year's resolution: reindented code in function package

provide simp and induct rules in Function.info

more official data record Function.info

simplified

absorb structures Decompose and Descent into Termination, to simplify further restructuring

another legacy "asm_lr"

merged

removed legacy asm_lr

merged

added lemmas

added lemma

removed FIXME

tuned error handling;

Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;

Download URLs -- with progress monitor.

Future values -- Scala version.

added simple dialogs;

added is_ready;

simplified init message -- removed redundant session property;

removed obsolete version check -- sanity delegated to Isabelle_System; tuned;

eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;

tuned signature;

less ambitious isatest for SML/NJ;

killed a few warnings

more regular axiom of infinity, with no (indirect) reference to overloaded constants

back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;

removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;

explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;

tuned;

crude Cygwin.setup;

ignore undefined environment;

separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);

tuned;

system shutdown hook: strict kill;

moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);

pid without newline -- required for Scala version of system_out;

higher-order treatment of temporary files;

isabelle_tool: apply platform_path only once; tuned;

slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");

some sanity checks for symbol interpretation;

allow UTF-8 in theory and file names;

factored-out Library.decode_permissive_utf8;

read header by scanning/parsing file;

quoted_content: handle escapes;

scan: operate on file (via Scan.byte_reader), more robust exception handling;

added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

removed unused read_file;

tidied proofs

made sml/nj happy

updated certificates

updated example

merged verification condition structure and term representation in one datatype, extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths), simplified discharging of verification conditions (due to improved datatype), added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)

merged

updated generated document sources

take care for destructive print mode properly using dedicated pretty builders

merged

made sml/nj happy

merged

dropped junk

reduced code generator cache to the baremost minimum

updated documentation

updated generated examples

reduced code generator cache to the baremost minimum; corrected spelling

basic setup for header scanning/parsing;

clarified atom parser: return content; added tags parser;

tuned;

renamed class Outer_Keyword to Outer_Syntax; renamed tokenize to scan (cf. ML version);

Isabelle session manager -- most basic setup;

actually closer file reader;

tuned;

added plain read_file;

consider proper input only; added wrappers;

added completion -- lazy avoids excessive table building; tuned signature;

Generic parsers for Isabelle/Isar outer syntax -- Scala version.

class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;

explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure; added Token_Reader; tuned;

Changes in generated code, apparently caused by changes to the code generation system itself.

Polishing up the English

merged

merged

clarified various user-defined syntax issues

prefer prefix "iso" over potentially misleading "is"; tuned

moved lemmas o_eq_dest, o_eq_elim here

add 'morphisms' option to domain_isomorphism command

merged

generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs

rename equals_zero_I to minus_unique (keep old name too)

add lemma swap_triple

improve performance by reordering of parser combinators;

added nested comments; tuned;

more Scala sources;

simiplified result of keyword parser (again); sort completions by plain string order; moved Reverse to library.scala;

simplified result of keyword and symbols parser; some support for parsing outer syntax tokens;

Outer lexical syntax for Isabelle/Isar -- Scala version.

refined some Symbol operations/signatures; tuned;

refined some Symbol operations/signatures; added Symbol.Matcher; flexible Scan.Lexicon.symbols, with one/many/many1 variants;

added basic library -- Scala version; added extra support for exceptions -- Scala version; moved exn.ML to accompany exn.scala;