Result: added STDOUT, SIGNAL; renamed method destroy to kill; method kill: close--sleep--destroy; tuned;

option -m: avoid additional quoting;

tuned whitespace;

proper termination of stdout thread; tuned;

added exit thread; added destroy method; tuned;

tuned diagnostics;

run Isabelle process with plain tty interaction;

added output protocol specification; PID: always on new line;

tuned;

added isatool tty;

added ISABELLE_LINE_EDITOR setting;

added ISABELLE_LINE_EDITOR; tuned;

* isatool tty runs Isabelle process with plain tty interaction;

nested commands: avoid nested errors;

added close_witness;

removed syntax in locale left_commutative

changed order in class parameters

heutistics for type annotations in Haskell

simplified

memorizing and exporting destruction rules

improved rule calculation

exported axiomsN

added div/mod examples

target language div and mod

clarified heading

dropped ws

added lemma

isatool codegen now returns exit value

a fold operation for multisets + more lemmas

tuned

adjusted

pretty for instantiation and overloading

continued

error handling for pathological cases

dropped induction rule

dropped Class.prep_spec

moved lemma odd_pos to theory Parity

joined StarClasses theory with StarDef

joined EvenOdd theory with Parity

tuned

added simple primitive note

moved instance parameter management from class.ML to axclass.ML

tuned header

switched import from Main to List

switched import from Main to PreList

explicit import of theory ATP_Linkup

explicit import of theory Main

swtiched ATP_Linkup and PreList in theory hierarchy

ML_OPTIONS="-H 1500" -- potentially works around GC core dump;

added Id, some cleanup

tuned message;

renamed IsabelleResult to IsabelleProcess.Result;

Isabelle process wrapper for JVM platform (tentative implementation in Java, which is to be replaced by a sane source language eventually);

tuned messages;

Isar loop: recover after toplevel crashes;

secure_main: enforces terminator, to gain robustness;

text_of: make double sure that result is well-formed, to avoid recurrent failures;

ML_OPTIONS="-H 1000" -- potentially works around GC core dump;

added off-line parse; read: no recovery on non-interactive source, yields proper errors;

(alt)string: allow explicit character codes (as in ML);

added nested 'Isabelle.command';

updated;

special_end: replaced Z by dot;

output_prompt: CRITICAL;

declaration of instance parameter names

exported declare_names

new primrec

instantiation target rather than legacy instance

proper treatment of code theorems for primrec

dropped Instance.instantiate

Adding "ex/Induction_Scheme.thy" to tests

experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)

tuned further

renamed ML_PID to PID;

R&F: added sgn lemma Prefix: sledge-hammered

temporary code generator work arounds

fixed slip

-authentic primrec

dropped legacy bindings

authentic primrec

dropped void space

added new primrec package

load sum_tree.ML

factored out handling of sum types again

added test_markup; added channel markup and specials;

moved basic test_markup to isabelle_process.ML;

added channels; added markup operation, which operates on plain strings instead of raw output;

replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;

check persistent sessions;

tuned signature;

made SML/NJ happy;

removed -e flag from most sessions;

instance int,real :: lordered_ring

methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.

tuned class parts

dropped Classpackage.thy

tuned

added parser for multi_arity

added constrain_thm

canonical instantiation

map_product and fold_product

interface and distinct simproc tuned

improved

interpretation of typedefs

simplified infrastructure for code generator operational equality

added something about instantiation target

switch poly to 5.1, removed -e flag from most sessions

switch at-poly main to poly 5.1

make mac-poly non-experimental

make at64 non-experimental

Isabelle process wrapper -- interaction via external program.

Toplevel.loop: explicit argument for secure loop, no warning on quit;

added Isar.secure_main; pass Secure.is_secure to Toplevel.loop;

added Tools/isabelle_process.ML;

isabelle process: replaced option -p by -W (process wrapper);

replaced option -p by -W (process wrapper); tuned PGIP option setup;

\<chi> is now considered a letter; tuned;

symbol chi is also a letter;

improvements

overloading target