1998-06-20 wenzelm 1998-06-20 export mk_triple1/2;
1998-06-20 wenzelm 1998-06-20 added read_def_axm;
1998-06-20 wenzelm 1998-06-20 added fix_mixfix;
1998-06-19 paulson 1998-06-19 fixed comment
1998-06-19 paulson 1998-06-19 tidying
1998-06-19 paulson 1998-06-19 New example Kerberos_BAN by G Bella
1998-06-18 wenzelm 1998-06-18 fixed comment;
1998-06-18 wenzelm 1998-06-18 tuned \s pattern;
1998-06-18 wenzelm 1998-06-18 isatool fixgoal;
1998-06-18 wenzelm 1998-06-18 removed Thy; the_context made public;
1998-06-18 wenzelm 1998-06-18 replaced warning by error_msg;
1998-06-18 wenzelm 1998-06-18 new toplevel commands `Goal' and `Goalw'; isatool fixgoal;
1998-06-18 wenzelm 1998-06-18 renamed thm(s) to Thm(s);
1998-06-18 wenzelm 1998-06-18 replace goal(w) commands by implicit versions Goal(w);
1998-06-17 nipkow 1998-06-17 Goal and Goalw
1998-06-17 nipkow 1998-06-17 goal -> Goal
1998-06-17 nipkow 1998-06-17 Changed and changed back.
1998-06-17 nipkow 1998-06-17 Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
1998-06-16 wenzelm 1998-06-16 added General/history.ML;
1998-06-16 wenzelm 1998-06-16 Histories of values, with undo and redo;
1998-06-15 wenzelm 1998-06-15 use_text replaces use_strings;
1998-06-15 wenzelm 1998-06-15 handle_error: capture error msgs, even if no exception raised;
1998-06-13 wenzelm 1998-06-13 removed use_text;
1998-06-12 wenzelm 1998-06-12 added use_text;
1998-06-12 wenzelm 1998-06-12 Context.add_session;
1998-06-12 wenzelm 1998-06-12 changed (| |) syntax to (: :);
1998-06-12 wenzelm 1998-06-12 changed {: :} syntax to (| |);
1998-06-12 wenzelm 1998-06-12 tuned exports; added Thy;
1998-06-11 nipkow 1998-06-11 removed rel.ML
1998-06-11 nipkow 1998-06-11 ancient relic
1998-06-10 wenzelm 1998-06-10 Context.the_context;
1998-06-10 wenzelm 1998-06-10 get_context renamed to the_context; added get_context, set_context;
1998-06-10 wenzelm 1998-06-10 tuned transaction;
1998-06-10 wenzelm 1998-06-10 tuned comments;
1998-06-10 wenzelm 1998-06-10 adapted to TheoryDataFun interface;
1998-06-10 wenzelm 1998-06-10 moved attributes theory data to Isar/isar_thy.ML;
1998-06-10 wenzelm 1998-06-10 moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;
1998-06-10 wenzelm 1998-06-10 added exnMessage;
1998-06-10 wenzelm 1998-06-10 added General;
1998-06-10 wenzelm 1998-06-10 added of_file;
1998-06-10 wenzelm 1998-06-10 General tools.
1998-06-10 wenzelm 1998-06-10 moved table.ML, object.ML, seq.ML, name_space.ML to General;
1998-06-10 wenzelm 1998-06-10 moved object.ML to General/object.ML;
1998-06-10 wenzelm 1998-06-10 moved table.ML to General/table.ML;
1998-06-10 wenzelm 1998-06-10 moved seq.ML to General/seq.ML;
1998-06-10 wenzelm 1998-06-10 moved position.ML, path.ML, file.ML to General;
1998-06-10 wenzelm 1998-06-10 moved name_space.ML to General/name_space.ML;
1998-06-10 wenzelm 1998-06-10 moved Thy/path.ML to General/path.ML;
1998-06-10 wenzelm 1998-06-10 moved Thy/position.ML to General/position.ML;
1998-06-10 wenzelm 1998-06-10 moved Thy/file.ML to General/file.ML;
1998-06-10 wenzelm 1998-06-10 new type-safe user interface for theory data;
1998-06-09 wenzelm 1998-06-09 nonterminals prog;
1998-06-09 wenzelm 1998-06-09 adapted to new theory data interface;
1998-06-08 wenzelm 1998-06-08 use type-safe theory data interface;
1998-06-08 wenzelm 1998-06-08 added theory_data.ML;
1998-06-08 wenzelm 1998-06-08 Type-safe interface for theory data.
1998-06-05 wenzelm 1998-06-05 * improved the theory data mechanism to support real encapsulation; main change of the internal interfaces: data kind name (string) replaced by private Object.kind, acting as authorization key;
1998-06-05 wenzelm 1998-06-05 accomodate tuned version of theory data;
1998-06-05 wenzelm 1998-06-05 added print_theorems: theory -> unit; added print_theory: theory -> unit; added transaction mechanism as last resort to accomodate non-atomic transformers (please avoid such things); tuned setup;
1998-06-05 wenzelm 1998-06-05 Object.T;