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

Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.

Added trans_tac (see Provers/nat_transitive.ML)

Solves simple arithmetic goals.

Subst as modified by Konrad Slind

Konrad Slind's TFL

New version of Yahalom, as recommended on p 259 of BAN paper

Addition of Reveal message

Deleted obsolete rewrites (they are now in HOL/simpdata)

Reveal -> Revl

The new proof of the lemma for new_nonces_not_seen is faster

Generaly tidying up

Important correction to comment

Replaced excluded_middle_tac by case_tac; tidied proofs

Tidied up the proof of A_trust_NS4

Replaced excluded_middle_tac by case_tac

Moving the CPUtimer declaration into cond_timeit should prevent the problems that caused exn TIME to be raised

Now checks that $LISTEN is set

Defined pred using nat_case rather than nat_rec. Added expand_nat_case

corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25)

bound o_apply theorem to thy

Removed extraneous spaces from all Makefiles

changed prettyprinting of ==>

Removed extraneous spaces from all Makefiles

Removed call to obsolete totalCPUTimer function

Addition of Sequents; removal of Modal and LK

Addition of OtwayRees_AN

Abadi and Needham's variant of Otway-Rees

Deleted obsolete clasets

Added comments describing better proofs

Simpset removes the de Morgan laws

Removed Modal since Sequents contains everything in it

Removed LK since Sequents contains everything in it

New root file with more description, and merging LK and Modal to Sequents

Tidied some proofs: changed needed for de Morgan laws

Addition of de Morgan laws

Removed Fast_tac made redundant by addition of de Morgan laws

Fuller description of examples

Plain text README files now redundant due to HTML versions

New version of axiom sees1_Says: Previously it only allowed the SENDER to see the content of messages... Now instead the RECIPIENT sees the messages. This change had no effect on subsequent proofs because protocol rules refer specifically to the relevant messages sent to an agent.

Plain text README files now redundant due to HTML versions

cond_timeit now catches exception Time, which sml/nj sometimes raised for no obvious reason

Updated references

Added the de Morgan laws (incl quantifier versions) to basic simpset

New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)

Put in the theorem Says_Crypt_not_lost

Put in a simpler and *much* faster proof of no_nonce_OR1_OR2

New guarantees for each line of protocol

Addition of Revl rule, and tidying

New theorem Crypt_imp_invKey_keysFor

Removed command made redundant by the new one-point rules

Introduction of Slow_tac and Slow_best_tac

Addition of one-point quantifier rewrite rules

Simple tidying

New proof required by change to simpdata.ML

Now replaces shorthand commands even if indented

New theorem Crypt_Fake_parts_insert

Simplified a proof

New comment in header

Tidied up some proofs

Ran expandshort

Removed commands made redundant by new one-point rules

Ran expandshort