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;

patched sum_case;

Obsolete because JDK 1.1.x contains a class ScrollPane

Updated to JDK 1.1.x

Proof mods due to eta contraction during rewriting.

Eta contraction is now performed all the time during rewriting.

currently disabled;

*** empty log message ***

made many specification operators infix

eliminated theory UNITY/Traces

improper simp methods;

tuned;

fold / unfold methods;

tuned;

no Toplevel.print for by, ., ..;

improved print_state;

verbose flag;

use_thy_only made pervasive;

added Isar_examples/NatSum.thy;

Old stuff.

proper quiet_mode; tuned messages;

adapted add_inductive, add_record;

adapted add_inductive;

intrs attributes;

proper quiet_mode;

iff_add_global (from simpdata.ML);

support forward chaining;

tuned;

added Isar_examples/Cantor.ML;

hol_setup, simpdata_setup;

"iff" attribute; simpdata_setup;

hol_setup;

"!" made keyword;

opt_thm_name: name optional;

added oooo;

fixed a bug many years old in rule plusEC

tuned msgs; outer syntax;

tuned;

tuned;

elaborated;

tuned;

tuned antiquotations;

improved 'single' method; added 'contradiction' method;

added thus, hence;

added FINISHED, same_tac;

use /usr/share and /usr/bin;

Now for recdefs that omit the WF relation; removed the separation between draft and theory modes

Now for recdefs that omit the WF relation

Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml

chgrp isabelle;

detailed proofs;

tuned;

oops;

fixed IO;

improved load paths;

single method: include not_elim, imp_elim;

more graceful handling of load paths;

improved auto dir handling;

tuned;

make Isabelle rpm packages for Linux/x86 from the distribution;

use_thy etc.: may specify path prefix, which is temporarily used as load path;

switch_theory: Context.pass;

recdef (TFL) now requires theory Recdef;

recdef requires theory Recdef;

tuned;

rep_datatype syntax: 'induction' instead of 'induct';

add_recdef: actual simpset; add_recdef_x: named simpset;

recdef adapted to RecdefPackage.add_recdef;

Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; Sign.base_name fid;

added ex and Modelcheck

tuned;

added for mucke translation;