SML/NJ startup script (for 0.93).

added smlnj-0.93;

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

added needs_filtered_use;

added write_charnames';

now uses SymbolInput.use;

symbol_input.ML: Defines 'use' command with symbol input filtering.

added symbol_input.ML;

fixed comment;

fixed comments;

now passes ML_SYSTEM as ml_system;

added symbolinput filter;

symbolinput - translate symbols into \<...> sequences;

renamed to symbolinput.pl;

renamed from symbol_input.pl;

minor tuning;

now fails if getsettings not found;

adaptions for symbol font

adaptions for symbol font

minor adaptions

added header

now also loads etc/isa-settings.el;

now discgarb called only for changed databases;

added set inclusion symbol syntax;

added warning for unprintable chars in strings;

fixed warning;

added typed print translations;

removed chartrans_of; added typed print translations; error msg for _appl(C) loop;

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.