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;

renamed P.ml_source to P.ML_source;

report doc_source;

added ML_source, doc_source;

antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;

added source_of';

P.doc_source and P.ml_sorce for proper SymbolPos.text;

oracle, header/local_theory/proof_markup: pass SymbolPos.text;

use SymbolPos.T list directly, instead of encoded SymbolPos.text;

ML_Context.add_antiq: pass position; @{lemma}: set source position;

ML_Context.add_antiq: pass position;

retrieve_thms: transfer fact position to result; tuned;

moved basic thm operations from structure PureThy to Thm; added position operations; tuned;

moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);

made SML/NJ happy;

removed obsolete present_html -- now part of regular theory presentation;

removed obsolete verbatim_source, results, chapter, section etc.; removed obsolete results, theorems(s); moved theorem result hook to proof_display.ML;

removed obsolete verbatim_source, results, chapter, section etc.; removed redundant end_index, end_theory;

ProofDisplay.add_hook;

simplified present_local_theory/proof;

ProofDisplay.theory_results;

removed obsolete present_results; added theory_results, which is subject to hooks (formerly in present.ML);

scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);

load_thy: no untabify (preserve position information!), present spans instead of verbatim source;

simplified markup commands;

simplified markup commands -- removed obsolete Present.results, always check text;

added untabify_content;

tuned;

removed obsolete untabify (superceded by SymbolPos.tabify_content);

tuned document;

removed obsolete theorems; handle generic XML markup as well (plain <markup> instead of <... class=markup>); misc tuning/update according to Pure/Generic/markup.ML;

Changed proof of strong induction rule to avoid infinite loop when premises of introduction rules contain equations.

token_kind_markup: complete coverage;

OuterSyntax.scan: pass position;

message: ignored if body empty;

load_thy: removed obsolete dir argument;

abstract type span, tuned interfaces; added report_token, report_span; markup ident tokens;

adapted ThyEdit operations;

added ignored, malformed transitions;

Symbol.source/OuterLex.source: more explicit do_recover argument; scan: pass position; removed obsolete prepare_command (now inlined in isar_syn.ML); renamed prepare_command_failsafe to prepare_command, reports tokens; load_thy: now based on ThyEdit operations, reports tokens and spans; tuned;

Isabelle.command: inline former OuterSyntax.prepare_command; Isar.command: based on fail-safe OuterSyntax.prepare_command;

load thy_edit.ML before outer_syntax.ML;

renamed unknown_span to malformed_span; added ident; tuned;

Symbol.source/OuterLex.source: more explicit do_recover argument;

updated generated file;

rudimentary code setup for set operations

<applet>: more XHTML 1.0 Transitional conformance;

Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;

<pre>: removed xml:space, is already default; result(s): avoid improper nesting of <pre> within <p>;

produce XHTML 1.0 Transitional; tuned charset name; renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!

changed code setup

re-arranged class dense_linear_order

rudimentary code setup for set operations

moved class wellorder to theory Orderings

added parse_token (from proof_context.ML);

read_tyname/const/const_proper: report position; moved parse_token to syntax.ML; tuned;

pass position to get_fact; tuned;

pass token source to typ/term etc.;

added name property operation; added local_fact; renamed proposition to prop (again);

renamed ML_Lex.val_of to content_of;

unified Args.T with OuterLex.token, renamed some operations; moved thm_sel to attrib.ML;

unified Args.T with OuterLex.token; RESET_VALUE of primitive parsers; export keyword_with; renamed keyword_sid to keyword_ident_or_symbolic; added int (from args.ML); added enum(1)', and_list(1)' (formerly in args.ML); removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);

unified Args.T with OuterLex.token; renamed val_of to content_of; added InternalValue kind; added datatype value/slot with static binding (from args.ML); renamed is_sid to ident_or_symbolic;

unified Args.T with OuterLex.token, renamed some operations; removed obsolete parse_args (cf. parse);

unified Args.T with OuterLex.token, renamed some operations; unified version of thm_sel (formerly in args.ML and spec_parse.ML);

unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);

load args.ML later (after outer_parse.ML);

unified Args.T with OuterLex.token, renamed some operations;

read_asts: report literal tokens;

tuned error message;

pos_of_token: Position.T; removed unused display_token; tuned;

dest: sort strings; report: Output.status;

added literal;