updated generated file;

wf_finite_psubset[simp], in_finite_psubset[simp]

Public interface to interpretation morphism.

moved term_of syntax to separate theory

removed obsolete theory

added quickcheck.ML

tuned comments;

multithreading for Poly/ML 5.1 is no longer supported;

tuned;

updated system manual;

Proof General / Emacs interface wrapper;

Proof General: option -I is obsolete;

added PROOFGENERAL_HOME;

separate emacs tool for Proof General / Emacs;

added quickcheck stub

removed babel again

celver code lemma avoid type ambiguity problem with Haskell

a sophisticated char/nibble conversion combinator

moved term_of syntax to separate theory

SimpleThread.fork;

Simplified thread fork interface.

added Concurrent/simple_thread.ML;

updated generated file;

misc tuning and modernization;

check setting and tool; added file;

Clearer separation of interpretation frontend and backend.

No interpretation of locale with dangling type frees.

Do not rely on locale assumption in interpretation.

The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.

Fixed typo in locale declaration.

added babel

explicit size of characters

dropped superfluous code lemmas

evaluation using code generator

generic value command

converted symbols.tex;

tuned;

converted misc.tex;

tuned;

generated files;

converted present.tex;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

load underscore package after iman etc.;

tuned comment;

added formal markup for setting, executable, tool;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

converted basics.tex to theory file;

added isatt markup;

New outline for codegen tutorial -- draft

added extern_fact (local or global); more procise printing of fact names;

print raw (internal) result names;

more procise printing of fact names;

pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;

cancel, shutdown: notify_all;

finish: Future.shutdown last;

eliminated requests, use global state variables uniformly; more robust shutdown;

finish: Future.shutdown;

added is_empty;

shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;

added focus, which indicates a particular collection of high-priority tasks; tuned;

some general notes on future values;

separate Concurrent/ROOT.ML;

Parallel list combinators.

added Concurrent/par_list.ML;

added interrupt_task (external id); tuned signature;

tuned;

future_schedule: uninterruptible join;

added future_scheduler (default false);

replaced join_all by join_results, which returns Exn.results; join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;

workers: explicit activity flag; SYNCHRONIZED: optional tracing;

future: allow explicit group; cancel: invalidate group identifier for all future members; tuned comments; tuned;

cancel: invalidate group implicitly, via bool ref; job: moved ok flag into group; added interrupt, interrupt_external for tasks;

auto_flush: uniform block buffering for all output streams;

auto_flush stdout, stderr as well;

proper values of no_interrupts, regular_interrupts;

cancel: check_scheduler; adapted to simplified TaskQueue.cancel; improved join/join_all: actively work towards results, i.e. do not yield unnecessarily; misc tuning;

simplified dequeue: provide Thread.self internally; simplified cancel: interrupt running threads internally; added depend; added dequeue_towards; misc tuning;

eliminated cache, access queue efficiently via IntGraph.get_first;

export get_first from underlying table;

out_stream: block-buffered, with separate autoflush thread (every 50ms);

babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;

added comment

human-readable printing of TaskQueue.task/group;

* Changed defaults for unify configuration options;

inherit group from running thread, or create a new one -- make it harder to re-use canceled groups; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;

job: explicit 'ok' status -- false for canceled jobs; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;

Overall exception handler in order to insulate our users from low-level bugs.

more careful exception handling in order to prevent backtracking; miscellaneous tidying up.

Increasing the default limits in order to prevent unnecessary failures.

send: broadcast condition while locked!

proper signature constraint;

tuned Mailbox.send;

removed unused sync_interrupts;

moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;

more interrupt operations; maintain thread data (formerly in task_queue.ML); wait: added tracing; added requests mailbox; handle excessive workers fork: inherit group; added rudimentary shutdown; misc tuning;

moved task, thread_data, group, queue to task_queue.ML; tuned signature; SYNCHRONIZED notify_all! misc tuning;

Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;

added Concurrent/task_queue.ML;

await: SYNCHRONIZED wait!

tuned check_cache; removed broken self_synchronized, which cannot be used in conjunction with condition variables; more precise use of SYNCHRONIZED vs. wait; tuned worker_loop;

added sync_interrupts, regular_interrupts; max_thread_value: enforce >= 1;

added sync_interrupts, regular_interrupts;

opaque signature constraint abstracts local type abbrev;

tuned;

added change_result;

Functional threads as future values.

added Concurrent/future.ML;

Default (mostly dummy) implementation of thread structures. formerly in multithreading.ML; create mutexes / condition variables without failure;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed dummy thread structures from multithreading.ML;

*** empty log message ***

explicit use of universal.ML and dummy_thread.ML;

added no_interrupts; tuned;

added no_interrupts; moved dummy thread structures to dummy_thread.ML;

tuned;

send: broadcast to all waiting threads;

added ML-Systems/thread_dummy.ML;

dropped "run" marker in monad syntax

multithreading.ML provides dummy thread structures;

different bookkeeping for code equations

renamed structure CodeTarget to Code_Target

instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel

proper header;

added receive_timeout; tuned comments;

check WRAPPER_OUTPUT node type;

init: disallow "" as out stream;

fixed deps: no Concurrent/receiver.ML yet;

Concurrent message exchange via mailbox -- with unbounded queueing.

added Concurrent/mailbox.ML;

reorganize subsections

rename INF_drop_prefix to INFM_drop_prefix

add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1

move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add

tuned signature;

added General/queue.ML;

Efficient queues.

moved Multithreading.task/schedule to Concurrent/schedule.ML

multithreading.ML provides dummy thread structures;

moved Multithreading.task/schedule to Concurrent/schedule.ML;

provide dummy thread structures, including proper Thread.getLocal/setLocal; moved task/schedule to Concurrent/schedule.ML;

Thread.getLocal/setLocal;

Scheduling -- multiple threads working on a queue of tasks. formerly in ML-Systems/multithreading_polyml.ML; simplified -- less tracing; use regular Isabelle/ML functions instead of NJ stuff;

added Concurrent/schedule.ML;

update tags

use /home/isabelle/mercurial/bin/hg wrapper;

exclude large .mov files;

simplified add_axiom: no hyps;

discontinued local axioms -- too difficult to implement, too easy to produce nonsense;

axiomatization is now global-only;

added const_decl;

simplified specify_const: canonical args, global deps;

declare_const: Name.binding, store/report position;

Sign.declare_const: Name.binding;

removed ex/Puzzle

added qualified: string -> binding -> binding;

Name.qualified;

theorem dependency hook: check previous state;

added pos_of;

-> AFP

simplified Toplevel.add_hook: cover successful transactions only;

retired Ben Porter's DenumRat in favour of the shorter proof in Real/Rational.thy

made SML/NJ happy;

refined theorem dependency output: previous state needs to contain a theory (not empty toplevel); new_thms_deps: explicity theory values;

* Generic Toplevel.add_hook interface allows to analyze the result of transactions (including failed ones). For example, see src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency output of transactions resulting in a new theory state.

Replaced Library/NatPair by Nat_Int_Bij.

added new_thms_deps (operates on global facts, some name_hint approximation); theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;

theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;

added add_hook interface for post-transition hooks;

tuned;

ProofDisplay.print_results;

no pervasive bindings; removed theory_results and related hook; print_results: ignore empty/internal kind -- like former theory_results;

Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.

distributed literal code generation out of central infrastructure

* Result facts now refer to the *full* internal name;

* Name bindings in higher specification mechanisms;

pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);

updated generated file;

Interpretation commands no longer accept interpretation attributes.

type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;

explicit type Name.binding for higher-specification elements;

explicit type Name.binding for higher-specification elements; report local_fact_decl, fixed_decl; simplified ProofContext.inferred_param;

explicit type Name.binding for higher-specification elements; added binding, parbinding;

explicit type Name.binding for higher-specification elements; simplified ProofContext.inferred_param;

explicit type Name.binding for higher-specification elements; name/var morphism operates on Name.binding;

added binding; thm_name/opt_thm_name: Name.binding;

added fixed_decl, fact_decl, local_fact_decl;

name_thm etc.: pass position; note_thms etc.: Name.binding, report fact_decl;

added type binding -- generic name bindings;

name/var morphism operates on Name.binding;

adapted to class instantiation compliance

It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...

renamed lemma

moved more lemmas here from AFP/Integration/Rats

moved lemma into SetInterval where it belongs

cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong

*** empty log message ***

extended interface to preferences to allow adding new ones

Prover is set via menu now

restructured code generation of literals

IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo; IsabelleSystem.exec: varargs convenience; more robust message thread management: no interrupt, but proper rendezvous via fifo (rm_fifo removes unused fifo, if isabelle-process fails);

init: more explicit protocol of open/remove rendezvous;

use hardwired /tmp -- fifo only work on local file-system;

separate module for code output

fixed names of class assumptions

dropped parameter prefix for class theorems

added charset (from isabelle_process.scala); added fifo_reader -- also works on Cygwin;

moved charset to isabelle_system.scala; IsabelleSystem.fifo_reader;

provide HOME_JVM=HOME to prevent implicit cygpath mangling;

restructured and split code serializer module

no parameter prefix for class interpretation

updated

tuned fold_lines;

fold_lines: simplified, more efficient due to String.fields;

rm fifo after open;

dummy setup for completion;

create named pipe;

added is_cygwin; added exec2, which joins stdout/stderr; tuned thread arrangement;

join stdout/stderr, eliminated Kind.STDERR; messages are read from separate fifo (ensures that spurious stdout from shell wrappers, Poly/ML runtime system etc. do not spoil message protocol); private output, output_raw;

explicit output stream, typically a named pipe;

refined option -W: output stream;

more function -> fun

quicksort: function -> fun

corrected some typos

fixed atom_to_xml: literal "name" attribute;

exported atom_to_xml;

changed Markup print mode to YXML -- explicitly decode messages before being issued; changed Output print mode to plain default -- no escaping; simplified pgml_sym: produce Pgml.pgmlatom, no special treatment of Ctrl/Raw; removed unused issue_pgips; removed obsolete delay_msgs feature -- the script parser never fails, but produces inline error markup; removed obsolete wrap_pgml; explicit transformation of messages (pgml_terms and message_content); remove obsolete split_markup workaround; misc tuning;

tuned;

present_token: disable print_mode, which is YXML now;

text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;

removed obsolete XML.Output workaround;

added get_int;

removed obsolete get_string; moved get_int to property.ML;

removed obsolete ProofGeneral/pgml_isabelle.ML;

simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)

renamed Buffer.write to File.write_buffer; added scalable iterator fold_lines; tuned;

renamed Buffer.write to File.write_buffer;

load buffer.ML before file.ML;

replaced find_substring by first_field;

Consistent naming of theorems in interpretation.

simplified parse_attrib (find_substring instead of space_explode);

added find_substring;

added HOL/ex/Numeral.thy

get rid of tabs;

Property lists.

added General/properties.ML;

type Properties.T;

proper error message

proper handling of type variabl names

completing arities after subclass instance

untabification

tuned code generator setup

added equivariance lemmas for ex1 and the

add lemmas about Rats similar to those about Reals

move real_vector class proofs into vector_space and group_hom locales

added distributivity of relation composition over union [simp]

tuned append;

command: symbols.encode;

Reorganisation of registration code.

function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes

purge classes after compilation;

renamed Isabelle-repository to isabelle;

Defined rationals (Rats) globally in Rational. Chractarized them with a few lemmas in RealDef, one of them from Sqrt.

replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;

moved new Symbol.Interpretation into plugin;

promoted to EBPlugin; tuned;

explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;

tuned;

isabelle process: pick options/args from properties;

removed unused ConsolePlugin dependency; added menu item; added some Isabelle options;

simplified exceptions: use plain error function / RuntimeException;

added try_result;

misc reorganization; simplified consumer thread; more robust stop;

Kind: added is_control; more robust kill/exit; tuned interfaces;

get: allow null;

misc tuning of names;

rearranged source files;

init_message: class markup in message body, not header;

repackaged as isabelle.jedit;

untabify: silently turn tab into space if column information is unavailable;

corrected cache handling for class operations

default replaces arbitrary

tuned import order

activated \<A>, \<a>, \<AA>, \<aa>; disabled \<RR>, \<II> which overlap with codepoints for \<Re>, \<Im>, remapped to unofficial place within Isabelle font;

* Isabelle/lib/classes/Pure.jar; * Status messages; * Homegrown Isabelle font;

jars: removed obsolete Java process wrapper (cf. new Pure.jar);

obsolete;

obsolete -- superceded by Pure.jar (Scala version);

updated to Pure.jar;

added exec; private posix_prefix;

moved class Result into static object, removed dynamic tree method; removed unused Symbol.Interpretation; class Result: added is_raw, is_system; disabled console echo; added interrupt, kill; IsabelleSystem.exec;

symbolic message markup; init message: class property;

renamed Markup.MALFORMED to Markup.BAD;

added position, messages; renamed messages to content, malformed to bad;

added messages and process information;

Position properties.

added General/position.scala;

adapted to new IsabelleProcess from Pure.jar; IsabellePlugin.result_content decodes symbols;

include ../../classes/Pure.jar;

added const Rational added more function puzzles

YXML.parse_failsafe; removed full_markup, YXML mode (default); renamed output_command to command; renamed output_ML to ML; tuned;

shell_prefix: physical /bin/env on Cygwin;

removed full_markup mode (default); removed YXML mode (default); added XML mode; message: class attribute, fail for malformed YXML;

added parse_failsafe;

refer to symbolic Markup;

Common markup elements.

added General/markup.scala;

BadVariable: toString;

use java.util.concurrent.LinkedBlockingQueue, which blocks as required; IsabelleProcessException: toString; Result: improved toString; Result: raw markup for stdout/stderr; cmdline: proper executable name, added YXML mode;

append_string: proper backslash in character escapes;

added getenv; renamed get_setting to getenv_strict; added shell_prefix (for Cygwin);

tuned;

Isabelle outer syntax.

added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala; scalac -deprecation;

Isabelle process management -- always reactive due to multi-threaded I/O.

renamed DOM to document, add xml version and optional stylesheets;

tuned comments; added document object model (DOM);

parse_attrib: proper index of name end!

tuned parse performance: avoid splitting terminal Y chunk;

parse_attrib: more efficient due to indexOf('=');

replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);

tuned comment;

added iterator over content;

proper ISABELLE_ROOT_JVM on Cygwin;

pattern: proper "." not "[.]"! tuned;

recode: proper result for unmatched symbols;

more robust pattern: look at longer matches first, added catch-all case; more private fields; reworked Recoder: more direct char/string operations, avoids inefficiency of large alternatives (java.util.regex does not optimize regexps);

added get_setting; removed obsolete ISABELLE_HOME, ISABELLE_HOME_USER; added platform_path, which expands variables and performs basic cygwin conversion;

read_symbols: proper IsabelleSystem.platform_path;

added ISABELLE_ROOT_JVM; removed obsolete ISABELLE_HOME_JVM, ISABELLE_HOME_USER_JVM;

Theorem on polynomial division and lemmas.

removed parse_element -- no longer fits to liberal parse!

Minimalistic XML tree values.

Efficient text representation of XML trees.

added General/xml.scala, General/yxml.scala;

decode escaped symbols as well; tuned;

tuned Recoder;

more private fields;

jar: invoke scaladoc;

tuned comments; simplified symbol pattern presentation: no need to keep source strings, canonical ofString does the job; auxiliary class Recoder; proper implementation of Interpretation.decode/encode;

use scala.collection.jcl.HashMap, which seems to be more efficient; char_pattern: proper matching of surrogate unicode characters, those outside the Basic Multilingual Plane; class Interpretation: misc reorganization, more serious preparation of patterns and tables;

jar target: removed jvmpath -- does not work on Linux!?

add scala-library.jar if available;

jar target: jvmpath;

Isabelle system support.

reading symbol interpretation tables;

added Tools/isabelle_system.scala;

removed unused usage;

more robust handling of directory layout variants;

refined scala/java wrappers via isatool;

tuned abbrevs;

added ISABELLE_SCALA, ISABELLE_JAVA;

added ISABELLE_HOME_JVM;

proper jvmpath for cygwin;

proper RC;

refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;

refined JVM path wrappers;

added JVM components (Scala or Java);

tuned;

jars: build Pure.jar;

scan: proper recovery for escaped \\< symbols;

basic setup for Scala material; added General/symbol.scala;

Basic support for Isabelle symbols.

added some abbrevs; \<euro>: from default font;

removed redundant "symbol" property; added "font" propery; disabled alternative letters (\<A> etc.) for now;

Default interpretation of some Isabelle symbols.

report antiquotation names; tuned messages;

fixed DOCTYPE -- XHTML is case-sensitive!

report antiquotation names;

added ML_antiq, doc_antiq;

added README;

generated truetype font;

The Jerusalem font from 2004 -- unicode version.

args: explicit groups for file_name, theory_name;

read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;

filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;

token_kind: add Space, Comment; tokenize: now includes improper tokens, cf. is_proper; added report_token;

renamed T.source_of' to T.source_position_of; tuned signature;

renamed T.source_of' to T.source_position_of;

output_markup: check Markup.is_none;

added is_none; added inner_comment;

Args.name_source(_position) for proper position information;

[source=false] for quoted antiquotation avoids quote-escapes in output;

report antiquotations;

tuned;

report ML_source;