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;

added mk_UNIV;

tuned;

simplified exporter interface;

added implies_intr_goals;

tuned;

Tuned.

Removed exit command from end of main method.

PS method now calculates layout using default font metrics.

Inserted table for character widths.

tuned induction proofs;

dest_env: norm_term on rhs;

typedef: export result;

ignore typedef result;

declare projected induction rules stemming from nested recursion;

TypedefPackage.add_typedef_no_result;

tuned;

* HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);

option -o FILE --output to FILE (ps, eps, pdf);

ISABELLE_EPSTOPDF="epstopdf";

Font metrics used for batch mode layout (without X11 connection).

Added support for batch mode layout (without X11 connection).

tuned;

improved induct;

be more careful about token class markers;

proper order of kind names;

support impromptu terminology of cases parameters;

parser for underscore (actually a symbolic identifier!);

allow empty set/type name;

simplified resolveq_cases_tac for cases, separate version for induct; divinate instantiation of induct rules; tuned;

tuned;

canonical 'cases'/'induct' rules for n-tuples (n=3..7)

canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)

setsum syntax;

intro! and elim! rules;

tuned NetRules;

Tactic.orderlist;

ObjectLogic.rulify;

Tactic.rewrite_cterm;

GPLed;

ring instead of ringS;

ring includes plus_ac0;

tuned;

support weight;

bang_args;

qualify some names;

map_nth_elem;

renamed reset_locs to del_locs

moved rulify to ObjectLogic;

moved rulify to ObjectLogic;

added qed_spec_mp etc.;

unified rewrite/rewrite_cterm/simplify interface;

tuned rewrite/simplify interface;

improved atomize setup;

atomize_tac etc. moved to object_logic.ML;

use ObjectLogic;

added 'atomize' attribute;

tuned full_rewrite;

ObjectLogic.setup;

tuned;

added object_logic.ML;

fixed auto steps (due to changed atomize);

Specifics about common object-logics.

use ObjectLogic stuff;

"HOL.mono";

ObjectLogic.atomize_tac;

improved atomize setup;

removed Ord;

removed Ord.thy (now part of HOL.thy).

judgment Trueprop; proper declarations of atomize rules; incorporate theory Ord; proper section and text markup; tuned;

added ML bindings from former theory Ord;

eliminated atomize rules;

judgment Trueprop; proper declarations of atomize rules;

updated;

* HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;

'morphisms' spec; tuned goal pattern for set;

tuned;

generic theorem kinds;

generic theorem kinds ("theorem", "lemma" etc.);

IsarThy.theorem_i Drule.internalK;

Drule.tag_internal;

* Pure: added 'corollary' command;

Tuned comment.

- Exported goals_conv and fconv_rule - Added forall_conv