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;