added extend_trfunsT; removed test: prtabs_of; removed chartrans;

added fix_tr', syn_ext_trfunsT; changed syn_ext_trfuns (fix_tr');

binder_tr': applied fix_tr';

Dummy change to document the change in revision 1.5: Parent theory changed to HOLCF.thy (former Tr2.thy) . Was necessary because the use of HOLCF_ss in Hoare.ML, which has been extended by the introduction of the Lift theories.

ex/Hoare.thy

Removed needless quotation marks

Streamlined many proofs

Temporary additions (random) for the nested Otway-Rees protocol They will need to be rationalized

Streamlined some proofs

Streamlined many proofs

Addition of the Hash constructor Strengthening spy_analz_tac

fixed alternative quantifier symbol syntax;

Now target "test" builds and tests TFL

ROOT file for TFL (needed for use_dir to work)

removed ambiguous symbols syntax;

fixed pris of binder syntax;

fixed pris of binder syntax;

added chartrans; prmode: added 'inout' option;

added chartrans_of;

mfix_to_xprod: now uses read_charnames;

tokenize: no gets exploded char list;

added read_charnames, write_charnames;

*** empty log message ***

syntax section: added 'output' mode option;

add_modesyntax(_i): added 'inout' argument;

symbol_input.pl - translate symbols into \<...> sequences.

Headers added

Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy

simpset extension moved from HOLCF.ML to One.ML and Tr2.ML

added theorems

qed_spec_mp moved to end of file

added DVI_VIEWER for 600dpi fonts;

Contents - list of available documentation;

patch-scripts.bash - relocate interpreter paths of Isabelle scripts.

various fixes;

*** empty log message ***

added -norc option;

getplatform - bash source script to augment current env;

added ISABELLE_DOCS;

added -norc option; error output to stderr;

added -norc option; error output to stderr; removed -o option; changed -u ML text;

Compatibility file for Standard ML of New Jersey, version 1.09.

Compatibility file for Poly/ML (versions 2.x, 3.x).

*** empty log message ***

mk - build Pure Isabelle.

removed escaping of 8bit chars;

comitting symlinks failed!!!

renamed from POLY.ML;

added -norc option;

added -norc option; error output to stderr;

findlogics: collect heap names from ISABELLE_PATH;

doc: view Isabelle documentation;

Minor renamings

MLWorks compatibility: it sort of works

Added public-key examples for Auth

Minor renamings

Moved much common material to Message.ML

Updating of banner

Loads new public-key examples

Minor speedups

Trivial renamings

Trivial renamings

Updated a comment

Moved much common material to Message.ML

Updating of comments

Public-key examples

added pwd;

fixed commit emulation;

changed font menu;

replaced cat by ucat; fixed RC handling;

replaced cat by ucat;

*** empty log message ***

fails more gracefully;

fixed ML_HOME;

added ISAMODE_HOME;

improved 'not found' messages;

*** empty log message ***

ucat - uninterruptible cat NOTE: If perl is unavailable we simply fall back on normal cat!

Emacs / Isamode interface.

Simplified file_info using OS.FileSys instead of Posix.FileSys (also for MLWorks compatibility)

Random number generated "downgraded" to generate numbers below 2^29 - 1, for MLWorks compatibility

run-smlnj: SML/NJ startup script (for 1.06 or later).

run-polyml: Poly/ML startup script.

isa-xterm: Isabelle within an xterm.

getsettings: bash source script to augment current env.

isabelle symbol fonts;

installfonts: install Isabelle symbol fonts.

getenv: get value from Isabelle settings.

changeparent: change parent of Poly/ML database.

settings: Isabelle settings -- site defaults.

isatool: Isabelle tool starter -- keeps your PATH name space clean.

isabelle: Basic Isabelle startup script.

removed 8bit sections

replaced Lift3 by Up3, moving Lift3.p to Up3.p

in Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg

Made comments more explicit

Removal of needless occurrences of "op"

removed out-dated comment;

removed;

Swapped arguments of Crypt (for clarity and because it is conventional)

Swapping arguments of Crypt; removing argument lost

added qed_spec_mp (from HOL);

Ring Theory.

Moved the Rings stuff from ex to Integ and showed that int::cring.

Modified dependencies for ex and Integ. (Rings)

*** empty log message ***

moved Lift*.* to Up*.*, renaming of all constans and theorems concerned, (*lift* to *up*, except Ilift to Ifup, lift to fup)

modified file headers renamed lift to fup

renamed is_flat to flat, moved Lift*.* to Up*.*, renaming of all constans and theorems concerned, (*lift* to *up*, except Ilift to Ifup, lift to fup)

Addition of Woo-Lam protocol

Fixed spelling error

Tidying and renaming of function Dom

Declares List_ as a synonym for List

Replaced map...~~ by ListPair.map

Extra fix needed in newN case

Missing case in instantiation of Transitivity prover (negate(None)=None)

Replaced map...~~ by ListPair.map Tried to tidy up the indenting...

Replaced map...~~ by ListPair.map

Addition of structures List and ListPair

Weaking of injectivity assumptions for newK and newN: they are no longer assumed injective over all traces, merely over the length of a trace