src/Pure/theory.ML
1999-05-17 wenzelm 1999-05-17 prep_ext exported (again);
1999-05-04 wenzelm 1999-05-04 hide prep_ext, merge_theories;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-03-17 wenzelm 1999-03-17 added assert_super;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-02-03 wenzelm 1999-02-03 added is_draft; renamed sig to PRIVATE_THEORY;
1998-11-17 wenzelm 1998-11-17 Theory.apply replaced by Library.apply;
1998-11-14 wenzelm 1998-11-14 val copy: theory -> theory;
1998-11-09 wenzelm 1998-11-09 removed local_theory;
1998-10-13 wenzelm 1998-10-13 PRIVATE sig parts;
1998-06-20 wenzelm 1998-06-20 added read_def_axm;
1998-06-10 wenzelm 1998-06-10 tuned comments;
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-05-28 wenzelm 1998-05-28 fixed error msgs;
1998-05-27 paulson 1998-05-27 Changed require to requires for MLWorks
1998-05-12 wenzelm 1998-05-12 fixed comment;
1998-04-29 wenzelm 1998-04-29 renamed setup to apply; added add_nonterminals: bstring list -> theory -> theory; added parent_path: theory -> theory; added root_path: theory -> theory; added require: theory -> string -> string -> unit (from section_utils.ML);
1998-04-04 wenzelm 1998-04-04 added local_theory (for Isar); added setup;
1998-02-12 wenzelm 1998-02-12 Sign.merge vs. Sign.nontriv_merge;
1998-02-12 wenzelm 1998-02-12 tuned add_trrules;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend;
1997-12-02 wenzelm 1997-12-02 tuned trfuns types;
1997-11-20 wenzelm 1997-11-20 init_data: improved print method;
1997-11-20 wenzelm 1997-11-20 tuned infer_types interface;
1997-11-05 wenzelm 1997-11-05 adapted add_trfunsT; defs: admit TYPE arguments;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-10-30 wenzelm 1997-10-30 tuned init_data;
1997-10-28 wenzelm 1997-10-28 added ancestors;
1997-10-24 wenzelm 1997-10-24 tuned names; tuned prep_ext_merge;
1997-10-23 wenzelm 1997-10-23 tuned;
1997-10-21 wenzelm 1997-10-21 sg_ref: automatic adjustment of thms of draft theories;
1997-10-20 wenzelm 1997-10-20 tuned types;
1997-10-20 wenzelm 1997-10-20 fixed types of add_XXX;
1997-10-16 wenzelm 1997-10-16 added merge_theories (new name arg);
1997-10-15 wenzelm 1997-10-15 remove merge_theories; merge_list: always prepares extend -- no longer supports aliasing merges;
1997-10-14 wenzelm 1997-10-14 added init_data, get_data, put_data;
1997-10-09 wenzelm 1997-10-09 improved oracles: named, many per theory; name spaces: thmK, oracleK;
1997-10-07 wenzelm 1997-10-07 improved types of add_XXX funs (xtyp etc.);
1997-10-06 wenzelm 1997-10-06 new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i added add_path, add_space; eliminated raise_term;
1997-10-01 wenzelm 1997-10-01 moved theory stuff (add_defs etc.) here from drule.ML; only BasicTheory opened;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-02-28 wenzelm 1997-02-28 added add_tokentrfuns;
1996-12-13 wenzelm 1996-12-13 added typed print translations;
1996-12-10 wenzelm 1996-12-10 add_modesyntax(_i): added 'inout' argument;
1996-11-19 wenzelm 1996-11-19 added add_modesyntax(_i);
1996-09-06 paulson 1996-09-06 Improved error handling: if there are syntax or type-checking errors, prints the name of the offending axiom
1996-03-05 paulson 1996-03-05 Addition of oracles
1996-02-29 paulson 1996-02-29 New file of just the theory primitives