remove codegen_process.pdf from distribution;

fixed wrong treatment of type variables in instantiation target

switched to Poly/ML 5.2;

doc test now runs on linux

added at-poly-5.1-para-e;

adjusted location of cambridge website

switch from gtar to tar

send from linux systems as well

tikz: change to pgfsys-dvi.def for plain dvi output;

replaced (*<*)(*>*) by invisibility tags;

updated generated file;

updated generated file;

work within *this* directory;

moved labels into actual sections;

removed TEXPATH, just chdir to Locales/document;

renamed expression: plain ~ (space) instead of \colon;

updated generated file;

replaced strange \: by \colon to make it work again on macbroy20-29;

updated generated file;

clarification of "subst" by Lucas Dixon;

use polyml-5.2;

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