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

Speedups involving norm

Introduction of structure Int

Updated and clearer(?) instructions

Modified formal of thms in html file.

removed 'open Syntax Type';

removed silly message;

subsig tuning;

tuned subsig;

Updated version and date

Removal of polymorphic equality via mem, subset, eq_set, etc

In-lined the one function call to normTsh

Removal of polymorphic equality via mem, subset, eq_set, etc

Now moves all Tool/*gif files.

Changed some mem calls to be monomorphic

Changed some mem, ins and union calls to be monomorphic

Changed some mem and ins calls to be monomorphic

Updated syntax; shortened comments; put in monomorphic versions of ins

Removed a call to polymorphic mem

Added a comment

Should never have been added in the first place

A bit of tidying up

Ran expandshort

Removed "standard" call from uresult, to allow specialist applications

Deleted a redundant pattern

Adjusting to new version of uresult

Tidying up: removing redundant assumptions, etc.

Deleted bogus comment

Adding lessI to default claset

tuned fix_shyps a little bit more;

New version of paper.

Replaced the very slow "find" command by "rm" with wildcards

Simplified new_keys_not_seen, etc.: replaced the union over all agents by the Spy alone. Proofs run faster and they do not have to be set up in terms of a previous lemma.

Used nat_trans_tac. New Eta. various smaller changes.

Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes

Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min

Minor changes to comments

New version with simpler disambiguation in YM3, Oops message, and no encryption in YM2

New, purely illustrative result Crypt_synth_analz

Proof of antisym_less_lift now simpler and more robust

Now uses Int.max instead of max

Changes tabs found in .thy files to spaces

Replaced "sum" (only usage?) by foldl op+

Now uses Int.max instead of max

maxidx_of_typs replaces max o map maxidx_of_typ

Now uses Int.max instead of max nodup_Vars now updates maxidx

maxidx_of_typs replaces max o map maxidx_of_typ Now uses Int.max instead of max

asm_rewrite_goal_tac now calls SELECT_GOAL. Replaced min by Int.min

Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML

Replaced min by Int.min

Deleted Olist constructor. Replaced minidx by "above" function

Now defines structure Int

Changed some mem calls to mem_int for greater efficiency (not that it could matter)

Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%

Changed some mem calls to mem_string for greater efficiency (not that it could matter)

Minor updates

Updated references

Minor corrections

Renamed and shuffled a few thms.

Simplified proofs

Tidied up a big mess in UN_parts_sees_Says

Changing from the Reveal to the Oops rule

Simplifid proofs.

Added (? x. t=x) = True

Documents the use of negative arguments to choplev and prlev

Changed comment to illustrate use of pathname

Allowing negative levels (as offsets) in prlev and choplev

New Oops message, with Server as source to ensure correct nonces

New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac

Two new protocol variants

Moved ex_strip_tac to the common part

Removal of unused predicate isSpy

Handles pathnames in ISABELLECOMP

Mentions the possibility of pathnames in ISABELLECOMP;

Creates a bigger main window

ISABELLECOMP may now have a leading pathname