added document;

simplified; header command;

strip_blanks;

got rid of most;

rep_datatype now stores theorems properly.

fixed title;

added document;

tuned comments;

tuned comment;

fixed ml_store_thm(s): deriv;

document preparation options: -c -d;

conditional url/hyperref setup;

present token source;

replace add_title by add_header;

clear_undo replaced by clear_undos; title replaced by header;

added is_toplevel;

clear: int argument;

use_dir: doc;

replaced clear_undo by clear_undos;

outer_lex.ML loaded in Thy;

include browser_info stuff; tex source presentation;

Simple LaTeX presentation primitives (based on outer lexical syntax).

begin_index: document; verbatim_source;

moved stuff to present.ML;

added Thy/latex.ML; removed Thy/browser_info.ML; use "../Isar/outer_lex.ML";

Got rid of readtm.

Tuned inductive definition.

updated;

added Thy/latex.ML; removed Thy/browser_info.ML (stuff now in Thy/present.ML);

Present.setup;

Added attribute rulify_prems (useful for modifying premises of introduction rules of inductive sets).

added copy_all; removed source;

clear: int arg;

added position;

Additional rules for inductive package.

added untabify;

Rule not_not is now stored in theory (needed by Inductive).

Monotonicity rules for inductive definitions can now be added to a theory via attribute "mono".

macros for Isabelle generated LaTeX output;

arithmetic now in IntArith;

simprocs now in IntArith;

IntArith;

Tools/typedef_package.ML;

eliminated ap/app;

proper dependencies of all theories and packages;

removed DatatypePackage.setup;

load / setup recdef package (TFL);

load / setup datatype package;

removed TFL/sys.sml; removed Integ/simproc.ML, Integ/bin_simprocs.ML; added Integ/IntArith.ML, Integ/IntArith.thy;

obsolete;

renamed 'prefix' to 'prfx' (avoids clash with infix);

tuned;

mk_frees, assume_read moved here; FOLogic.mk_conj, FOLogic.mk_disj;

tryres, gen_make_elim moved here;

FOLogic.mk_conj;

added mk_conj, mk_disj, mk_imp;