updated to official 5.2;

use isabelle style files from Doc/ -- not the generated ones (which are not present in the repository anyway);

some reorganization and fine-tuning;

some fine-tuning;

CodeTarget.target_code_width;

Tuned proof.

New version covering interpretation.

proper path to isabelle.jar;

reorganized isar-ref;

added Wenzel:2006:Festschrift;

class_deps: improper;

\cite{Wenzel:2006:Festschrift};

updated generated file;

moved stuff from pure.thy to Misc.thy;

obsolete;

updated generated file;

tuned;

updated generated file;

moved header command to Document_Preparation;

tuned structure;

moved header command here;

removed onsolete pure.thy (cf. Misc.thy);

updated generated file;

updated ML types for advanced translations;

moved (ax_)specification to end;

moved subst/hypsubst to "Basic proof tools"; tuned;

added Document_Preparation;

updated generated file;

tuned spacing;

major reorganization of document structure;

removed obsolete basics.tex;

more contributors; removed obsolete basics.tex; added Document_Preparation.tex;

renamed theory "syntax" to "Outer_Syntax";

isatool tty;

renamed theory "intro" to "Introduction";

tuned proofs

fixed bug: maxidx was wrongly calculuated from term, now calculated from theorem correctly.

new example

updated to E 0.999-006;

THIS_IS_ISABELLE_MAKEBIN is back;

cvs2cl only for unofficial releases;

more AFP sessions;

*** empty log message ***

Updated function tutorial.

(adjusted)

various code streamlining

more AFP sessions;

legacy_feature: no proof context in simpset;

proper context for attribute simplified;

added warning_count for issued reconstruction failure messages (limit 10); less nesting of let expressions;

proper context for ss;

proper context for simp_thms_conv;

added warning_count for issued reconstruction failure messages;

tuned;

*** empty log message ***

yet another attempt to circumvent printmode problems

obsolete;

moved README-polyml to polyml/README;

README for Poly/ML 5.2 distribution;

tuned;

more contribs;

misc tuning for Isabelle2008;

added some notable improvements;

tuned version numbers;

prepared for Isabelle2008;

added ISABELLE_HOME to startup; pathed OS.FileSys.tmpName to drop C string terminator; added OS.FileSys.fullPath;

added Substring.full;

moved distinctness_limit to datatype_rep_proofs.ML

fixed utterly wrong print mode handling

new serializer interface

added new code_datatype example

proper use of the Pretty module

permissive wrt. instantiation of class operations

proper lemma [source] antiquotation

check for illegal merge of class parameters

proper NoSubsort CLASS_ERROR

tuned theorem order

inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument; misc tuning -- more cterm operations, more qualified names;

updated generated file;

added local_theory command wrappers;

uniform treatment of target, not as config;

more uniform treatment of OuterSyntax.local_theory commands;

updated generated file;

invisible comment;

function: uniform treatment of target, not as config;

added parse_document (optional unchecked header material); parse: parse_document instead of parse_element;

exported master_directory;

present_excursion: setmp_thread_position during presentation;

use: explicit .ML;

ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;

fixed improper handling of return code (pdf and ps.gz formats)

add constants: set Markup.theory_nameN in tags;

added theory_nameN;

rearranged subsections

Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.

Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.

temporary adjustment

tuned

more permissive preprocessor

explicit type schemes for functions

moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs

added code for quantifiers

simplified proof

made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct

use_file: added str_of_pos argument (ignored);

Added entry explaining incompatibilities introduced by replacing sets by predicates.

instantiation lift :: (countable) bifinite

use new class package for classes profinite, bifinite; remove approx class

updated generated file;

unparse_term: check PureThy.old_appl_syntax instead of CPure;

theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;

converted to regular application syntax;

eliminated theory CPure;

setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;

* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.

proper handling of the return code for the ps-format (fixes a bug)

oops -- pr_graph = Syntax.string_of_term; removed dead pr_matrix;

command 'normal_form': proper context via Variable.auto_fixes;

moved global pretty/string_of functions from Sign to Syntax; reordered signature;

Syntax.string_of_sort: proper context;