-D generated;

Added "clean" target.

Fixed problem with batch mode layout, which caused an AWT exception when no X11 connection was available.

initBrowser now has additional noAWT argument.

Constructor no longer takes font as an argument.

Moved font settings from TreeNode to TreeBrowser.

Moved font settings from Vertex to GraphView.

deleted the redundant first argument of adjust(a,b)

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

New simproc, needed to cope with combinations of (abstract) 0, (abstract) 1, binary numerals in literal arithmetic.

Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.

keep DISPLAY;

updated;

renamed to Typedefs.thy to avoid conflict with main HOL version;

* proper spacing of consecutive markup elements, especially text blocks after section headings;

\newif\ifisamarkup controls spacing of isabeginpar;

improved spacing;

maintain Latex.flag_markup;

flag_markup;

Types/document/Typedefs;

renamed Typedef.thy to Typedefs.thy (former already present in main HOL);

got rid of separate root.tex;

graceful interpretation of -i/-d/-D options; verbose: additional messages/warnings; include document graph;

include document graph;

document graph option;

conditional: bool -> (unit -> unit) -> unit; std_error: string -> unit;

added TextIO.stdErr;

include document graph; tuned;

document graphs for several sessions;

tuned;

calculational rules moved from FOL to IFOL;

option -g for document graph; removed all presumptions about -d/-D (handled by isabelle process);

option -q also excludes -v true in generated stuff; tuned message;

dvips -q;

removed -v option (handled by isabelle process);

-o pdf: produce *both* eps and pdf; tuned;

* greatly simplified document preparation setup, including more graceful interpretation of isatool usedir -i/-d/-D options, and more instructive isatool mkdir; users should basically be able to get started with "isatool mkdir Test && isatool make"; * theory dependency graph may now be incorporated into documents; isatool usedir -g true will produce session_graph.eps/.pdf for use with \includegraphics of LaTeX;

got rid of ML proof scripts;

induct_method.ML -- proof by cases and induction on sets and types (Isar);

latex output: bold lambda;

got rid of ML proof scripts for Product_Type;

got rid of Provers/split_paired_all.ML;

improved default dependencies;

revert to proper version (!);

GPLed;

tuned;

use abstract product type instead of datatype;

moved atomize stuff to theory HOL;

legacy interfaces for axclass instantiation;

added map_base;

sane internal interfaces for instance;

sane internal interface for add_typedef(_i);

proper setup for abstract product types;

moved InductMethod.setup to theory HOL;

setup generic cases and induction (from Inductive.thy);

guillemot syntax;

improved internal interface of typedef;

abstract product types;

proper proof of split_paired_all (presently unused);

tuned comments;