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

moved split_tac

added symbols syntax;

added "op :", "op ~:" syntax; added symbols syntax;

added symbols syntax;

fixed comment; added "op <", "op <=" syntax; added symbol syntax;

moved "1", "2" to syntax section;

symbol names changes;

symbol name changes;

improved some symbol names;

changed symbolic char syntax to \<NAME>

use_thy now automatically opens theory structures;

renamed "symbolfont" to "symbols";

moved if_cancel to the right place

added if_cancel later to simpset

Updated instructions

Better indentation

Replaced obsolete "use" command

Compatibility with SML/NJ 109, and some compatibility with later versions

Now tries to delete SML/NJ .heap files

Converted I/O operatios for Basis Library compatibility

Eta-expanded some declarations that are illegal under value polymorphism Converted I/O operatios for Basis Library compatibility

Basis library emulation, especially of I/O operations

Removed an obsolete and incompatible declaration

Replaced obsolete "makestring" by Bool.toString

Replaced obsolete "makestring" by Int.toString

Eta-expanded some declarations that are illegal under value polymorphism

Replaced obsolete "use" command

Uses Basis Library equivalent of cd

Makefile improvements by Thomas Santen and Stephan Herrmann Should be more portable across different versions of make

if_cancel added to HOL_ss

Removed or eta-expanded some declarations that are illegal under value polymorphism

Checks for empty files. Replaces auto() calls

Eta-expansion of a function definition, for value polymorphism

Structure Bool and value Int.toString needed to replace makestring calls

Eta-expansion of a function definition, for value polymorphism

Eta-expansion of a function definition, for value polymorphism

Removal of needless function definition

Eta-expansion of a function definition, for value polymorphism

Added instructions on starting up

New material from Norbert Voelker for efficient binary comparisons

A bit of commutative ing theory, with a simplification tacxtic and an example.

Added Lagrang. Modified comment.

Replaced LK&Modal by Sequents

Updating of a reference (Ch. Paulin)

Minor textual improvements; updating of a reference

Have been obsolete for months; contents are now in Shared and NS_Shared

Basis library emulation for old ML compilers

Added warning message

Tidied up some proofs, ...

Minor reformatting

Further comments on versions of SML/NJ

plus -> Plus to avoid hiding class plus

restored changed prettyprinting of ==>;

removed old commented out text;

minor tuning;

tuned some char names;

added this file;

added add_modesyntax(_i);

added symbolfont syntax;

improved string scanner: converts 8 bit chars to escape sequences;

mixfix: added syntax for Infirl/rName; syntax section: added option printer table name;

extend_const_gram now supports multiple disjoint printer tables;

new delimiter syntax in mixfixes: \{SYMBOLNAME} is char from symbol font;

added print_mode: string list ref (order of printer tables); multiple disjoint printer tables, to be combined hierarchically; multiple entries in printer tables (matched in order);

added Infixl/rName: specify infix name independently from syntax; added Pure symbolfont syntax;

added symbol_font.ML;

added add_modesyntax(_i); improved syntax of ==, =?=, ==> (now allows "op ..."); added Pure symbolfont syntax;

added is_printable: string -> bool;

added Syntax/symbol_font.ML;

Removal of an obsolete result, and authentication of B to A

Changed subst_bounds to subst_bound, to run faster

Optimizations: removal of polymorphic equality; one-argument case for subst_bounds