added def_name; class_triv: Sign.sg;

added cond_extern_thm_sg; have_thmss: name made optional;

AxClass.setup;

axclass.ML loaded after Isar;

made weblint happy;

comment;

removed obsolete user data stuff; removed junk;

theory: include parent links;

outer syntax for 'datatype';

add_primrec(_i): attributes; outer syntax for 'primrec';

outer syntax for 'record'; proof method 'record_split';

named witnesses: PureThy.get_thmss; outer syntax for 'typedecl', 'typedef';

primrec: empty attributes;

tuned opt_mixfix failure;

add_title;

added 'title'; tuned names, comments;

tuned space;

comment;

workaround default_name problem;

removed foo_build_completed -- now handled by session management (via usedir);

include 'README'; tuned;

tuned;

moved Thy/session.ML to Isar/session.ML;

tuned;

-x option;

updated;

report session path; removed more junk;

report path instead of actual session;

HTML output;

maintain current/parent index; removed junk;

output: some symbol translations; removed insert_here, conclude_theory; added begin/end_index, theory_entry, session_entries;

parent_session;

allow meta_outer to do nothing

updating both Yahalom protocols to the Gets model

updated not_bad_tac for the Gets model

deleted obsolete comments

Present.theory_source;

begin/end_theory: presentation;

checkpoint -- basic functionality only;

added use_path; begin_theory: include files;

IsarThy.begin/end_theory;

Present.theorem;

fixed add_path reset; init / finish presentation;

still fake, passes BrowserInfo;

HTML markup elements.

added html.ML, browser_info.ML;

token translation: real;

added strlen_real, setmp_margin;

tuned using nth_elem_string, exists_string;

added make, dir;

added mkdir;

added Buffer;

simple string buffers;

*** empty log message ***

pretty_thm_no_quote;

HTML.setup;

added nth_elem_string, exists_string;

token translation: real;

tuned;

tidied

Added Bella's "Gets" model for Otway_Rees. Also affects some other theories. Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a translation.

Suc -> +1

modified zip

Fixed bug in add_datatype_axm: Recursion and case combinators were assigned inconsistent names in quick_and_dirty mode, which caused recdef etc. to crash.

fixed again;

expandshort

added UNITY/Extend

expandshort

tidied

UNITY fully working at last...

expandshort

new theory of extending the state space

fixed {ISABELLE};

removed the infernal States, eqStates, compatible, etc.

tidied

simpler proofs of congruence rules

new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq

simpler proofs of congruence rules

new image laws

added a commment on the "ext" rule

new theorems Pow_0 and Pow_insert; renamed other Pow theorems

added rev_bexI

fixed order of multiple -m options;

fixed geometry;

tidying in conjuntion with the TISSEC paper; replaced (unit option) by a new datatype (role)

new theorem image_Union_eq

foldl_string;

renamed space2 to spacespace

tuned pretty format lookup;

pretty_thm: quote terms (separately);

Symbol.output subject to print mode;

-m isabelle_font;

tuned;

Present.init;

init, finish;

proper handling of print_mode wrt. Pretty.sym;