tuned;

fixed named type infixes (actual BUG!);

updated isatool install;

-p option; -k option;

adapted isatool install;

improved isatool install;

tuned;

ML_PLATFORM;

ML_PLATFORM;

fixed @@;

fixed bib file

fixed;

new definition for nth. added warnings, if primrec definition is deleted from simpset.

useless relic

arith_tac

tuned;

common qed and end of proofs;

* New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P

New bounded quantifier syntax: !x<i. P etc

added new theory Yahalom_Bad

added new theory Yahalom_Bad

exchanged the order of Gets and Notes in datatype event

fixed thm_name again;

Theory.sign_of;

xnum token class;

xstr token class;

Theory.sign_of;

fixed axclass_tac;

tuned;

Theory.sign_of;

qualify Theory.sign_of etc.;

fixed msg;

tuned msg;

axclass_tac lost an argument;

HOL/typedef: fixed type inference for representing set; AxClass.axclass_tac lost the theory argument;

rep_datatype: '_i' version, attributes, outer syntax;

local open OuterParse;

actually check non-emptiness theorem; added typedef_proof(_i); 'typedef' outer syntax;

fixed typedef representing set;

adapted rep_datatype;

added dest_mem;

theory data; attributes for class axioms; instance_subclass/arity_proof(_i); expand_classes proof method; 'axclass' / 'instance' outer syntax;

adapted AxClass.add_axclass; PureThy.get_thm axioms;

tuned msgs; removed verbose flag;

tuned;

cleaned comments;

added apply_cond_open;

added (improper_)command;

added simple_arity, spec_name, spec_opt_name; tuned thm_name; xthms1: no 'and' separators;

added '_i' versions; add_constdefs; apply_theorems; fixed assume block nest;

OuterSyntax.(improper_)command; moved axclass / instance to Pure/axclass.ML; moved spec(') to outer_parse.ML;

added assert_super;

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;