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
1998-05-28 wenzelm 1998-05-28 fixed ml_prompts;
1998-05-28 wenzelm 1998-05-28 changed get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option;
1998-05-28 wenzelm 1998-05-28 tuned dist version;
1998-05-28 wenzelm 1998-05-28 tuned header;
1998-05-28 wenzelm 1998-05-28 version under control of Admin/makedist;
1998-05-28 wenzelm 1998-05-28 README, Pure/ROOT.ML: version set automatically;
1998-05-28 wenzelm 1998-05-28 version under control of Admin/makedist; ml_prompts;
1998-05-28 wenzelm 1998-05-28 added ml_prompts;
1998-05-28 wenzelm 1998-05-28 added mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source; (map)filter: fixed propagation of prompt;
1998-05-28 wenzelm 1998-05-28 tuned error msg;
1998-05-28 wenzelm 1998-05-28 fixed error msgs;
1998-05-27 paulson 1998-05-27 Structure Option now declared in MLWorks
1998-05-27 paulson 1998-05-27 mk_all_imp: no longer creates goals that have beta-redexes
1998-05-27 paulson 1998-05-27 more tracing
1998-05-27 paulson 1998-05-27 Changed require to requires for MLWorks
1998-05-27 paulson 1998-05-27 auto update
1998-05-26 wenzelm 1998-05-26 made SML/NJ happy;
1998-05-26 wenzelm 1998-05-26 foldl_map prep_field;
1998-05-25 wenzelm 1998-05-25 tuned store_theory;
1998-05-25 wenzelm 1998-05-25 tuned local, global; tuned begin and end theory;
1998-05-25 wenzelm 1998-05-25 tuned store_theory: theory -> unit;
1998-05-25 wenzelm 1998-05-25 added get_name, put_name, global_path, local_path, begin_theory, end_theory;
1998-05-25 wenzelm 1998-05-25 global_names moved to pure_thy.ML;
1998-05-25 wenzelm 1998-05-25 certify_term: type_check replaces Term.type_of, providing sensible error messages; eliminated mapfilt_atoms (use Term.foldl_aterms);
1998-05-25 wenzelm 1998-05-25 renamed state_source to source'; removed test;
1998-05-25 wenzelm 1998-05-25 added recover, source;
1998-05-25 wenzelm 1998-05-25 added catch: ('a -> 'b) -> 'a -> 'b; tuned source(');
1998-05-25 wenzelm 1998-05-25 remove seq2, scan (use seq2, foldl_map from library.ML);
1998-05-25 wenzelm 1998-05-25 added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list; added seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit; tuned 'beginning';
1998-05-25 nipkow 1998-05-25 Swapped order of params.
1998-05-20 wenzelm 1998-05-20 changed get_single: ('a, 'b) source -> 'a option * ('a, 'b) source; tuned prompt; Scan.source vs. Scan.source';
1998-05-20 wenzelm 1998-05-20 source vs. source';
1998-05-20 wenzelm 1998-05-20 tuned keywords;
1998-05-20 wenzelm 1998-05-20 added is_stale;
1998-05-20 wenzelm 1998-05-20 tuned signature; added pretty_theory;
1998-05-20 wenzelm 1998-05-20 tuned comments;
1998-05-20 wenzelm 1998-05-20 tuned;
1998-05-20 nipkow 1998-05-20 Small mods.
1998-05-19 wenzelm 1998-05-19 prompt made part of source;
1998-05-19 wenzelm 1998-05-19 fixed handle_error: cat_lines;
1998-05-19 wenzelm 1998-05-19 added Thy/position.ML;
1998-05-19 wenzelm 1998-05-19 added source: string -> (string, string list) Source.source;
1998-05-19 wenzelm 1998-05-19 Input positions.
1998-05-18 wenzelm 1998-05-18 added Syntax/source.ML;
1998-05-18 wenzelm 1998-05-18 added Source module;
1998-05-18 wenzelm 1998-05-18 Co-algebraic data sources.
1998-05-18 wenzelm 1998-05-18 Symbol.stopper;
1998-05-18 wenzelm 1998-05-18 improved finite scans: more abstract stopper; fixed source: now actually handles finite scans; tuned bulk;
1998-05-18 nipkow 1998-05-18 snoc_induct/exhaust -> rev_induct_exhaust.
1998-05-18 nipkow 1998-05-18 Cleaned up and simplified etc. snoc_induct/exhaust -> rev_induct_exhaust.
1998-05-15 wenzelm 1998-05-15 witnesses: lookup stored thms instead of axioms;
1998-05-15 wenzelm 1998-05-15 added add_axioms_x, add_defs_x;
1998-05-15 wenzelm 1998-05-15 PureThy.add_typedecls;
1998-05-14 nipkow 1998-05-14 Reordred arguments in AutoChopper. Updated README with ref to paper.
1998-05-14 oheimb 1998-05-14 extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info
1998-05-14 oheimb 1998-05-14 simplifications
1998-05-14 oheimb 1998-05-14 disabled (experimental) geometry option