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;
1998-06-05 wenzelm 1998-06-05 improved data: secure version using Object.T and Object.kind;
1998-06-05 wenzelm 1998-06-05 tuned setup; tuned add_attributes: comment; accomodate tuned version of data;
1998-06-05 wenzelm 1998-06-05 use Object.T and Object.kind; added print_data; improved get_data, put_data: more abstract; add_axioms(_i), add_oracle: made atomic transactions;
1998-06-05 wenzelm 1998-06-05 removed type object (see object.ML);
1998-06-05 wenzelm 1998-06-05 tuned print_exn;
1998-06-05 wenzelm 1998-06-05 print_data moved to theory.ML; print_theory: exclude theorems (no forward reference!);
1998-06-05 wenzelm 1998-06-05 added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq; added ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added EVERY: ('a -> 'a seq) list -> 'a -> 'a seq; added FIRST: ('a -> 'b seq) list -> 'a -> 'b seq; added TRY: ('a -> 'a seq) -> 'a -> 'a seq; added REPEAT: ('a -> 'a seq) -> 'a -> 'a seq;
1998-06-05 wenzelm 1998-06-05 added object.ML;
1998-06-02 oheimb 1998-06-02 added option_map_o_empty added option_map_o_empty and option_map_o_update to simpset()
1998-06-02 oheimb 1998-06-02 added split_etas
1998-06-02 oheimb 1998-06-02 added split_sum_case_asm
1998-05-29 wenzelm 1998-05-29 tuned;
1998-05-29 wenzelm 1998-05-29 tuned msgs;
1998-05-28 paulson 1998-05-28 auto update