fixed braces;

stylistic improvements

Documents directory Induct; stylistic improvements

New acknowledgements

fixed witness syntax;

SYNC;

New acknowledgements; fixed overfull lines and tables

New acknowledgements; no Fast_tac

Larry's private LaTeX-2e version

Moved induction examples to directory Induct

changed title to README

Documentation for directory "ex"

Documentation for directory "Induct"

Conversion to use blast_tac (with other improvements)

New directory to contain examples of (co)inductive definitions

Description of the Auth directory: security protocols proofs

fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);

tuned;

*** empty log message ***

tuned comments;

fixed simplifier ex;

SYNC;

fixed simplifier examples;

Stupid bug in induct_tac caused warning to always appear.

removed MLtrans, MLtext;

added \Pure, \CPure;

misc updates, tuning, cleanup;

tuned;

tuned;

Cosmetic update of induct_tac; test first now.

SYNC;

misc updates, tuning, cleanup;

Some blast_tac calls; more needed

Again "norm" DOES NOT normalize bodies of abstractions Showterm (used for tracing) now follows variable instantiations (in order to make up for the "norm" change)

fixed comment;

-P option (prune empty dirs);

Updated to LaTeX 2e

New version of rail.sty for LaTeX 2e

Updated to LaTeX 2e

Version of the proof macros for LaTeX 2e

This file is now replaced by proof.sty

Higher bound means much faster proof

More tracing. hyp_subst_tac allowed to fail

New blast_tac call: made possible by bug fix involving equality substitution

No longer proves mutual_induct unless it is necessary. Previous version proved it, then threw it away...

Documented blast_tac

Automatic update

Indexing for trace_simp

No longer proves mutual induction rules unless they are needed

Fixed clasets so that blast_tac would work

Now modified for sml/nj 109.27

More tracing; less exception handling

improved the space2 glyph;

added IOA (meta theory and ABP, NTP examples);

fixed Id;

removed (most of) IOA (see HOLCF/IOA);

old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);

moved to .. (see also new version in HOLCF/IOA/meta_theory);

removed -- new version in HOLCF/IOA/NTP;

remove -- new version in HOLCF/IOA/ABP;

New theorems Pow_in_Vfrom and Pow_in_VLimit

Old NTP files now running under the IOA meta theory based on HOLCF;

Old ABP files now running under the IOA meta theory based on HOLCF;

New meta theory for IOA based on HOLCF.

improved display of non-ASCII chars;

fixed enc_start;

deactivated new symbols (not yet printable on xterm, emacs);

renamed \<choice> to \<orelse>;

added \<orelse> symbols syntax for case;

added \<langle>, \<rangle> symbols syntax;

added new chars;

is_blank: added space2 (160);

improved DVI_VIEWER default;

improved tmp comment;

removed -norc;

used explcite tactics in instances (since ax_per_trans "loops")

changed Domain->Dom for SML/NJ

removed -c option;

removed -c option;

removed COPYDB flag;

removed -c option;

obsolete;

no longer forces default;

misc tuning;

removed one blank at end of line 37

refer to SOME, NONE on top-level;

adapted for 1.09.27 (and later);

open General (type option is in Option in the newer versions, but always the top-level);

adapted to SML/NJ 1.09.27; minor cleanup;

Added 'induct_tac'

Updates because nat_ind_tac no longer appends "1" to the ind.var.

removed space;

induct_tac

expandshort

Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...

get_thydata accesses the second component of the data field. This component used to be empty until set at the end of loading an ML file. Now the second component is already set when the thy file has ben read.