src/Pure/theory.ML
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;
2005-05-30 obua 2005-05-30 Infinite chains in definitions are now detected, too.
2005-05-29 obua 2005-05-29 Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
2005-04-16 wenzelm 2005-04-16 added del_modesyntax(_i);
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Sign.prep_ext_merge;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-09 wenzelm 2004-06-09 Sign.is_logtype;
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;
2004-05-21 wenzelm 2004-05-21 Type.strip_sorts;
2004-04-22 wenzelm 2004-04-22 support for advanced translation functions;
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-09-23 skalberg 2003-09-23 Fixed soundness bug.
2003-09-04 berghofe 2003-09-04 Changed no_vars such that it outputs list of illegal schematic variables.
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-21 wenzelm 2001-12-21 hide: flag for full/base name;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-08-15 wenzelm 2001-08-15 support for absolute namespace entry paths;
2001-01-18 wenzelm 2001-01-18 Sign.exists_stamp;
2000-11-18 wenzelm 2000-11-18 improved messages;
2000-11-06 wenzelm 2000-11-06 Sign.typ_instance;
2000-08-17 wenzelm 2000-08-17 tuned error handling;
2000-08-04 wenzelm 2000-08-04 axioms: Term.no_dummy_patterns;
2000-07-13 wenzelm 2000-07-13 tuned cycle_msg;
2000-07-13 wenzelm 2000-07-13 const_deps: unit Graph.T; proper merge of const_deps; tuned;
2000-07-08 nipkow 2000-07-08 Defs are now checked for circularity (if not overloaded).
2000-07-07 nipkow 2000-07-07 Tightened up check of types in constant defs.
2000-05-21 wenzelm 2000-05-21 adapted to inner syntax of sorts;
2000-04-17 wenzelm 2000-04-17 name space hide operations;
1999-07-12 wenzelm 1999-07-12 removed merge_theories;
1999-05-17 wenzelm 1999-05-17 prep_ext exported (again);
1999-05-04 wenzelm 1999-05-04 hide prep_ext, merge_theories;