src/Pure/pure_thy.ML
2008-03-15 wenzelm 2008-03-15 get_thm(s): check facts lookup vs. old thm database;
2008-03-15 wenzelm 2008-03-15 replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories); removed unused get_thm(s)_closure; removed obsolete fact_index_of, valid_thms, thms_containing(_consts);
2008-02-10 wenzelm 2008-02-10 maintain default position;
2008-01-26 wenzelm 2008-01-26 added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;
2007-12-10 haftmann 2007-12-10 added simple primitive note
2007-10-13 wenzelm 2007-10-13 replaced obsolete Theory.add_finals_i by Theory.add_deps;
2007-10-11 wenzelm 2007-10-11 removed obsolete simple_def;
2007-10-02 wenzelm 2007-10-02 removed unused add_defss;
2007-10-01 wenzelm 2007-10-01 NameSelection: more interval checks;
2007-09-30 wenzelm 2007-09-30 Sign.add_consts_authentic: tags (Markup.property list);
2007-09-25 wenzelm 2007-09-25 tuned functor application;
2007-08-27 haftmann 2007-08-27 added simple definition scheme
2007-08-13 wenzelm 2007-08-13 moved appl syntax to PureThy; SimpleSyntax.read_typ/term/prop;
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-28 wenzelm 2007-07-28 removed dead code;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections;
2007-07-08 wenzelm 2007-07-08 thm tag: Markup.property list;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-02-26 wenzelm 2007-02-26 Thm.internalK;
2007-02-26 wenzelm 2007-02-26 removed obsolete theorem_space;
2007-02-06 wenzelm 2007-02-06 added has_kind/get_kind; tuned;
2007-02-01 wenzelm 2007-02-01 proper use of PureThy.has_name_hint instead of hard-wired string'';
2007-01-31 aspinall 2007-01-31 Expose hard-wired string which was changed and broke Proof General.
2007-01-19 wenzelm 2007-01-19 moved thm/thms to ml_context.ML; moved generic_setup, add_oracle to isar_cmd.ML;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-12-30 wenzelm 2006-12-30 added has_name_hint; name_thm: more careful pre-naming;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-30 wenzelm 2006-11-30 Theory.merge_list;
2006-11-29 wenzelm 2006-11-29 *** bad commit -- reverted to previous version ***
2006-11-29 wenzelm 2006-11-29 added map/burrow_facts; exported name_multi, name_thm;
2006-11-29 wenzelm 2006-11-29 added map/burrow_facts; exported name_multi, name_thm;
2006-11-28 wenzelm 2006-11-28 added burrow_fact; no export of name_thms(s);
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-23 wenzelm 2006-11-23 tuned;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm; exported note_thms(s);
2006-10-04 haftmann 2006-10-04 *** empty log message ***
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 tuned exception handling;
2006-06-05 wenzelm 2006-06-05 support embedded terms;
2006-05-13 wenzelm 2006-05-13 added add_defs_unchecked(_i);
2006-05-05 wenzelm 2006-05-05 added syntax for _type_constraint_;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-04-13 wenzelm 2006-04-13 moved print_theorems/theory to Isar/proof_display.ML;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction, based on actual const;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-01-29 wenzelm 2006-01-29 proper order of trfuns;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);
2006-01-25 wenzelm 2006-01-25 export name_multi;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; added syntax (from Syntax/mixfix.ML); added HTML output syntax for _lambda;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 generic_setup: optional argument, defaults to Context.setup();
2006-01-07 wenzelm 2006-01-07 gen_names: preserve empty names;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy