src/Pure/pure_thy.ML
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-16 wenzelm 2008-10-16 added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-09-02 wenzelm 2008-09-02 name_thm etc.: pass position; note_thms etc.: Name.binding, report fact_decl;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-05 wenzelm 2008-08-05 get_fact: report position;
2008-08-04 wenzelm 2008-08-04 removed obsolete note_thms_cmd;
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-25 haftmann 2008-07-25 dropped PureThy.note; added PureThy.add_thm
2008-06-14 wenzelm 2008-06-14 removed old theorem database;
2008-05-18 wenzelm 2008-05-18 theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;
2008-04-16 wenzelm 2008-04-16 renamed check_fact to defined_fact;
2008-04-16 wenzelm 2008-04-16 removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;
2008-04-15 wenzelm 2008-04-15 added intern_fact, check_fact, hide_fact; renamed all_facts_of to facts_of; removed hide_thms; Sign.hide_const;
2008-04-15 wenzelm 2008-04-15 moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-03 wenzelm 2008-04-03 removed obsolete add_axiomss(_i);
2008-03-29 wenzelm 2008-03-29 eliminated destructive/critical theorem database; simplified store_thm(s); removed obsolete smart_store_thm(s); tuned;
2008-03-28 wenzelm 2008-03-28 NAMED_CRITICAL;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 tuned;
2008-03-27 wenzelm 2008-03-27 removed obsolete appl_syntax, applC_syntax;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; implicit setup of emerging theory Pure;
2008-03-25 wenzelm 2008-03-25 get fact: do not compare names;
2008-03-25 wenzelm 2008-03-25 support dynamic facts;
2008-03-20 wenzelm 2008-03-20 get_thms etc.: improved reporting of source position;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument; renamed former get_thms(_silent) to get_fact(_silent);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-18 wenzelm 2008-03-18 removed check_lookup; added get_thms_silent;
2008-03-18 wenzelm 2008-03-18 added ckeck_lookup flag (default false), which controls sanity check of thm lookup;
2008-03-17 wenzelm 2008-03-17 Facts.add_global;
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;