src/Pure/theory.ML
2007-09-29 wenzelm 2007-09-29 Sign.the_const_constraint;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read; no export of read/cert_axm;
2007-09-20 wenzelm 2007-09-20 tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers;
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-08-09 haftmann 2007-08-09 new access interface in defs.ML
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 removed comments -- no exception TERM; merge_list: exception THEORY;
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-15 wenzelm 2007-04-15 removed obsolete inferT_axm;
2007-04-14 wenzelm 2007-04-14 simplified read_axm;
2007-04-14 wenzelm 2007-04-14 tuned signature; added axiom_table, oracle_table; removed unused read_def_axm;
2007-04-04 wenzelm 2007-04-04 removed unused dep_graph;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-03-20 haftmann 2007-03-20 added theory dependency graph
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-11-30 wenzelm 2006-11-30 added merge_list;
2006-09-15 wenzelm 2006-09-15 removed type aliases for theory/theory_ref;
2006-08-17 haftmann 2006-08-17 dropped definitions_of
2006-07-19 wenzelm 2006-07-19 Sign.infer_types: Name.context;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-05-25 wenzelm 2006-05-25 tuned;
2006-05-24 wenzelm 2006-05-24 added add_deps, which actually records dependencies of consts (unlike add_finals); tuned;
2006-05-22 wenzelm 2006-05-22 Defs.specifications_of: lhs/rhs now use typargs;
2006-05-20 wenzelm 2006-05-20 tuned Defs interfaces;
2006-05-13 wenzelm 2006-05-13 Theory.add_defs(_i): added unchecked flag;
2006-05-11 wenzelm 2006-05-11 tuned Defs.merge;
2006-05-08 wenzelm 2006-05-08 Defs.define: const_typargs;
2006-05-05 wenzelm 2006-05-05 added definitions_of;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 tuned;
2006-02-25 haftmann 2006-02-25 added more detailed data to consts
2006-02-07 wenzelm 2006-02-07 adapted Sign.infer_types(_simult), Sign.certify_term/prop;
2006-02-06 wenzelm 2006-02-06 moved no_vars to sign.ML; removed dest_def (cf. Sign.cert_def);
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-24 wenzelm 2006-01-24 add_finals: prep_consts, i.e. varify type;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-02 wenzelm 2005-12-02 defs: beta/eta contract lhs;
2005-11-09 wenzelm 2005-11-09 tuned;
2005-09-29 wenzelm 2005-09-29 back to simple 'defs' (cf. revision 1.79); prep_const: Compress.type;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-08-09 haftmann 2005-08-09 exported dest_def
2005-08-01 wenzelm 2005-08-01 Compress.term;
2005-07-28 wenzelm 2005-07-28 check_overloading replaces datatype overloading; tuned;
2005-07-19 wenzelm 2005-07-19 tuned defs interface;
2005-07-13 wenzelm 2005-07-13 tuned;
2005-07-07 obua 2005-07-07 1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded
2005-06-29 wenzelm 2005-06-29 Syntax.read thy;
2005-06-22 wenzelm 2005-06-22 renamed init to init_data;
2005-06-20 wenzelm 2005-06-20 added begin_theory, end_theory;
2005-06-17 wenzelm 2005-06-17 type theory, theory_ref, exception THEORY and related operations imported from Context; actual theory content declared as theory data; removed syn_of; import theory operations in SIGN_THEORY from Sign; tuned;
2005-06-11 wenzelm 2005-06-11 renamed hide_classes/types/consts to hide_XXX_i; added separate hide_classes/types/consts; refer to name spaces values instead of names;
2005-06-09 wenzelm 2005-06-09 axioms and oracles: NameSpace.table; added axioms_of, all_axioms_of;
2005-06-07 obua 2005-06-07 A flag DEFS_CHAIN_HISTORY can be used to improve the error message in case a cycle has been detected. If it is switched off and a cycle has been detected, the user is notified that there is such a flag.
2005-06-05 wenzelm 2005-06-05 renamed const_deps to defs; improved error messages; major cleanup -- removed quite a bit of dead code;
2005-06-03 obua 2005-06-03 Integrates cycle detection in definitions with finalconsts
2005-06-02 wenzelm 2005-06-02 Sign.restore_naming; err_in_defn: do not apply Sign.full_name again; tuned;
2005-05-31 obua 2005-05-31 Removed final_consts from theory data. Now const_deps deals with final constants.
2005-05-31 wenzelm 2005-05-31 added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming; tuned;