1999-03-11 wenzelm 1999-03-11 named witnesses: PureThy.get_thmss; outer syntax for 'typedecl', 'typedef';
1999-03-11 wenzelm 1999-03-11 primrec: empty attributes;
1999-03-11 wenzelm 1999-03-11 tuned opt_mixfix failure;
1999-03-11 wenzelm 1999-03-11 add_title;
1999-03-11 wenzelm 1999-03-11 added 'title'; tuned names, comments;
1999-03-11 wenzelm 1999-03-11 tuned space;
1999-03-11 wenzelm 1999-03-11 comment;
1999-03-11 wenzelm 1999-03-11 workaround default_name problem;
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1999-03-11 wenzelm 1999-03-11 include 'README'; tuned;
1999-03-11 wenzelm 1999-03-11 tuned;
1999-03-11 wenzelm 1999-03-11 moved Thy/session.ML to Isar/session.ML;
1999-03-10 wenzelm 1999-03-10 tuned;
1999-03-10 wenzelm 1999-03-10 -x option;
1999-03-10 wenzelm 1999-03-10 updated;
1999-03-10 wenzelm 1999-03-10 report session path; removed more junk;
1999-03-10 wenzelm 1999-03-10 report path instead of actual session;
1999-03-10 wenzelm 1999-03-10 HTML output;
1999-03-10 wenzelm 1999-03-10 maintain current/parent index; removed junk;
1999-03-10 wenzelm 1999-03-10 output: some symbol translations; removed insert_here, conclude_theory; added begin/end_index, theory_entry, session_entries;
1999-03-10 wenzelm 1999-03-10 parent_session;
1999-03-10 paulson 1999-03-10 allow meta_outer to do nothing
1999-03-10 paulson 1999-03-10 updating both Yahalom protocols to the Gets model
1999-03-10 paulson 1999-03-10 updated not_bad_tac for the Gets model
1999-03-10 paulson 1999-03-10 deleted obsolete comments
1999-03-09 wenzelm 1999-03-09 Present.theory_source;
1999-03-09 wenzelm 1999-03-09 begin/end_theory: presentation;
1999-03-09 wenzelm 1999-03-09 checkpoint -- basic functionality only;
1999-03-09 wenzelm 1999-03-09 added use_path; begin_theory: include files;
1999-03-09 wenzelm 1999-03-09 IsarThy.begin/end_theory;
1999-03-09 wenzelm 1999-03-09 Present.theorem;
1999-03-09 wenzelm 1999-03-09 fixed add_path reset; init / finish presentation;
1999-03-09 wenzelm 1999-03-09 still fake, passes BrowserInfo;
1999-03-09 wenzelm 1999-03-09 HTML markup elements.
1999-03-09 wenzelm 1999-03-09 added html.ML, browser_info.ML;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-03-09 wenzelm 1999-03-09 added strlen_real, setmp_margin;
1999-03-09 wenzelm 1999-03-09 tuned using nth_elem_string, exists_string;
1999-03-09 wenzelm 1999-03-09 added make, dir;
1999-03-09 wenzelm 1999-03-09 added mkdir;
1999-03-09 wenzelm 1999-03-09 added Buffer;
1999-03-09 wenzelm 1999-03-09 simple string buffers;
1999-03-09 wenzelm 1999-03-09 *** empty log message ***
1999-03-09 wenzelm 1999-03-09 pretty_thm_no_quote;
1999-03-09 wenzelm 1999-03-09 HTML.setup;
1999-03-09 wenzelm 1999-03-09 added nth_elem_string, exists_string;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-03-09 wenzelm 1999-03-09 tuned;
1999-03-09 paulson 1999-03-09 tidied
1999-03-09 paulson 1999-03-09 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.
1999-03-08 nipkow 1999-03-08 Suc -> +1
1999-03-08 nipkow 1999-03-08 modified zip
1999-03-05 berghofe 1999-03-05 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.
1999-03-04 wenzelm 1999-03-04 fixed again;
1999-03-03 paulson 1999-03-03 expandshort
1999-03-03 paulson 1999-03-03 added UNITY/Extend
1999-03-03 paulson 1999-03-03 expandshort
1999-03-03 paulson 1999-03-03 tidied
1999-03-03 paulson 1999-03-03 UNITY fully working at last...
1999-03-03 paulson 1999-03-03 expandshort