Updated usage information for tool "usedir".

Theory browser stuff has been moved to "present.tex".

obsolete;

ISABELLE_USEDIR_OPTIONS="-i true"

Changed html data directory and names of graph files.

There is now one single option -i for generating theory browsing information instead of the two options -h and -g .

Modified some links.

Client, Server certificates now sent using the separate Certificate rule, simplifying ServerHello and ClientKeyExch. Resumption no longer needs its own version of ServerHello. Proofs run nearly three minutes faster.

tuned;

superficial;

obsolete;

margin 76 (2nd try :-);

fixed href to html library;

improved warning;

default margin 76 (to accomodate warning and error default output);

Step_tac -> Safe_tac

Much tidying including step_tac -> clarify_tac or safe_tac; sometimes used qed_spec_mp

Step_tac -> Safe_tac

Much tidying including "qed" instead of result(), and even qed_spec_mp, and Safe_tac instead of step_tac

Previously loaded the WRONG THEORY, ignoring Confluence...

Now using qed_spec_mp

result() -> qed; Step_tac -> Safe_tac

Step_tac -> Safe_tac

Renamed XA, XB to PA, PB and removed the certificate from Client Verify

Default simpset tactics now dereference "simpset" only when given the proof state

Added Safe_tac; all other default claset tactics now dereference "claset" only when given the proof state

fast_tac HOL_cs -> Fast_tac, etc.

result() -> qed

Step_tac -> Safe_tac

Tidied proof of r_comp_rtrancl_eq

qed_spec_mp, normalize_thm, etc. copied in from HOL.ML

Step_tac -> Safe_tac

Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt

Safe_tac; qed_spec_mp in FOL

Minor tidying to use Clarify_tac, etc.

eliminated rules; tuned;

Clarify_tac and some textual improvements

Clarify_tac; general reorganization

Deleted obsolete version of clarify_tac

Deleted the unused list_mk_disj

Deleted the unused gtake and recoded enumerate to use foldl

Deleted an obsolete step in TrustServerFinished

Deleted obsolete axioms inj_serverK and isSym_serverK

Tidied proofs, using Clarify_tac

Changed some proofs to use Clarify_tac

Prints warnings using the "warning" function instead of "writeln"

Generalized and exported biresolution_from_nets_tac to allow the declaration of Clarify_tac

Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac

sessionK now indexed by nat instead of bool. Weaker Oops conditions on final guarantees

Tidied some proofs using clarify_tac

clarify_tac and a new simprule

Names and saves the theorem parts_spies_subset_used

pure_trfuns: added constraint;

added handle_error: ('a -> 'b) -> 'a -> 'b error;

index.html obsolete;

Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);

acks;

added Cambridge fs;

fixed pttrn syntax;

fixed LAM <x,y,zs>.b syntax (may break some unusual cases);

tuned pattern syntax;

tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts vs. pttrn/pttrns;

fixed idt/idts vs. pttrn/pttrns;

Added Cambridge font server

obsolete;

Simplified SpyKeys to use sessionK instead of clientK and serverK Proved and used analz_insert_key, shortening scripts

First working version with Oops event for session keys

Full version of TLS including session resumption, but no Oops

Deleted the obsolete theorem analz_UN1_synth

Global change: lost->bad and sees Spy->spies First change just gives a more sensible name. Second change eliminates the agent parameter of "sees" to simplify definitions and theorems

Deleted the redundant identifier Says_imp_sees_Spy'

New proof of respond_Spy_not_see_session_key

Removed the simprule imp_disjL from the analz_image_..._ss to boost speed

Fixed comments

Spy can see Notes of the compromised agents

Now with the sessionK constant and new events ClientAccepts and ServerAccepts

Addition of SessionIDs to the Hello and Finished messages

Deleted the redundant simprule not_parts_not_analz

Deleted the redundant simprule not_parts_not_analz

Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification faster

TLS now with a distinction between premaster secret and master secret

extended adm_tac;

replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;

removed print_goals_ref (which was broken anyway);

Split base cases from "msg" to "atomic" in order to reduce the number of freeness theorems

Now uses the generic induct_tac

auto update

Added Larry's test for preventing a datatype shadowing a theory.

Example from HOLCF paper.

Loads HoareEx now.

adm_tac extended

moved extended adm_tac to new place

added ".ML" extension in "use" command

Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition

set_of_list

Deleted an obsolete description of rewrite_cterm. The current version uses meta-simpsets, which are undocumented