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
1999-03-03 paulson 1999-03-03 new theory of extending the state space
1999-03-01 wenzelm 1999-03-01 fixed {ISABELLE};
1999-03-01 paulson 1999-03-01 removed the infernal States, eqStates, compatible, etc.
1999-03-01 paulson 1999-03-01 tidied
1999-03-01 paulson 1999-03-01 simpler proofs of congruence rules
1999-03-01 paulson 1999-03-01 new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
1999-03-01 paulson 1999-03-01 simpler proofs of congruence rules
1999-02-22 paulson 1999-02-22 new image laws
1999-02-22 paulson 1999-02-22 added a commment on the "ext" rule
1999-02-22 paulson 1999-02-22 new theorems Pow_0 and Pow_insert; renamed other Pow theorems
1999-02-22 paulson 1999-02-22 added rev_bexI
1999-02-18 wenzelm 1999-02-18 fixed order of multiple -m options;
1999-02-18 grobauer 1999-02-18 fixed geometry;
1999-02-16 paulson 1999-02-16 tidying in conjuntion with the TISSEC paper; replaced (unit option) by a new datatype (role)
1999-02-16 paulson 1999-02-16 new theorem image_Union_eq
1999-02-13 wenzelm 1999-02-13 foldl_string;
1999-02-12 oheimb 1999-02-12 renamed space2 to spacespace
1999-02-12 wenzelm 1999-02-12 tuned pretty format lookup;
1999-02-12 wenzelm 1999-02-12 pretty_thm: quote terms (separately);
1999-02-11 wenzelm 1999-02-11 Symbol.output subject to print mode;
1999-02-11 wenzelm 1999-02-11 -m isabelle_font;
1999-02-11 wenzelm 1999-02-11 tuned;