ThyInfo.finalize_all renamed to ThyInfo.finish;

node_cases renamed to node_case;

prep_ext exported (again);

backup operation replaces transaction;

removed get_nodes; added keys; all_preds / all_succs: topological order; added del_nodes;

remove_thy;

tuned arrows;

Arrows are no longer needed because of redesign of the html pages.

Changed some file names.

Added function get_preds.

Added setup for BrowserInfo.

usedir now recognizes additional option -P which is used to tell the presentation module where to find *.html files of theories.

Changed interface of function use_dir.

Present.begin_theory now needs an additional argument of type theory to store information about session identifiers.

Reimplemented graph generator.

Added some code to enable browser to display remote documents.

new thm extend_JN; renamed extend_leadsto

"component" now an infix

indentation

tuned;

ad-hoc fix for bold indexes;

strip_quotes replaced by unenclose;

rearranged some modules;

rearranged order of modules;

Basic URLs.

added url.ML;

pdf setup;

tuned;

fixed msg;

moved scan.ML;

new comments, variable renaming, etc

tidied

changes for new manual.bib

make pdf;

tuned;

pdf setup;

cite HOLCF;

tuned;

axclass;

axclass; datatype;

pdf setup;

*** empty log message ***

*** empty log message ***

pdf setup;

fixed URLs;

pdf setup;

replaced png by pdf;

pdf pics;

tidied

tidied

new refererences for Inductive manual, but still incomplete

tuned;

pdf setup;

*** empty log message ***

pdf setup;

tuned;

More refs.

Refs.

New title page.

tuned;

manual.bib;

no rail;

fixed FILES;

improved Makefile;

improved Makefile;

isabelle.eps;

improved Makefile; no rail;

tuned;

improved Makefile;

*** empty log message ***

Common part for Doc Makefiles;

Now uses manual.bib; some references updated

tuned rpm file names;

updated docs;

Bibtex database for documentation.

Bibtex stuff.

*** empty log message ***

HOL;

removed HOL.tex;

tuned;

updated;

HOL part moved to 'logics-HOL' manual;

fixed;

used to be part of 'logics' manual;

isabelle_zf image;

*** empty log message ***

Arithmetic.

add_recdef: removed names / attributes;

new definitions of Co and LeadsTo

transaction: Theory.copy;

hide prep_ext, merge_theories;

oops;

tuned;

Invariant -> Always and other tidying

tuned;

theory loader stuff updated and improved;

fixed reqs?

improved error handling

renamed state variables

tidied

tuned;

prefer /bin for ./configure;

try chown root:root;

renamed 'dummy' to 'dummy_pattern' (less dangerous);

tuned;

method = meth3 (again);

peoper defer_recdef interface;

theory data: copy;

separated recdef / defer_recdef;

tuned defer_recdef interfaces;

comment, interest;

Comment.text;

comment sections; made "%" a keyword;

dummy patterns; theory data: copy;

added Isar/comment.ML;

val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;

theory data: copy; consts dummy :: 'a ("'_");

theory data: copy;

improved icons;

Isabelle icons;