src/Pure/Isar/proof_context.ML
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-16 wenzelm 2006-01-16 case_result: drop_schematic, i.e. be permissive about illegal binds;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag; mixfix: added Structure; renamed type exporter to export; removed obsolete sign_of; tuned signature; tuned;
2006-01-07 wenzelm 2006-01-07 added infer_type, declared_type;
2006-01-07 wenzelm 2006-01-07 support nested cases; tuned apply_case;
2005-12-22 wenzelm 2005-12-22 cases: main is_proper flag; print_cases: show proper cases only;
2005-12-17 wenzelm 2005-12-17 sort_distinct;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-08 wenzelm 2005-12-08 removed Syntax.deskolem;
2005-12-02 wenzelm 2005-12-02 removed fixed_tr: now handled in syntax module; replaced mixfix_typ by TypeInfer.mixfixT, which handles binders as well; def: beta/eta contract lhs;
2005-11-30 wenzelm 2005-11-30 match_bind(_i): return terms; mk_def: simultaneous defs; prepare_dummies: produce globally unique indexnames;
2005-11-25 wenzelm 2005-11-25 revert_skolem: fall back on Syntax.deskolem;
2005-11-19 wenzelm 2005-11-19 Goal.norm_hhf_protected;
2005-11-16 wenzelm 2005-11-16 added revert_skolem, mk_def, add_def; export: Goal.norm_hhf'; tuned;
2005-11-10 wenzelm 2005-11-10 moved find_free to term.ML;
2005-11-09 wenzelm 2005-11-09 tvars_intr_list: natural argument order;
2005-11-08 wenzelm 2005-11-08 removed export_plain; (some_)fact_tac: Drule.incr_indexes;
2005-10-28 wenzelm 2005-10-28 lthms_containing: not o valid_thms;
2005-10-28 wenzelm 2005-10-28 added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;
2005-10-21 wenzelm 2005-10-21 Goal.norm_hhf_rule;
2005-10-15 wenzelm 2005-10-15 note_thmss, read/cert_vars etc.: natural argument order; added string_of_thm; tuned;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-17 wenzelm 2005-09-17 added auto_fix (from proof.ML); added assms_of; removed assumptions_of; pretty_thm: show out-of-context hyps; warn_extra_tfrees: works again, tuned;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-14 wenzelm 2005-09-14 tuned;
2005-09-13 wenzelm 2005-09-13 added add_view, export_view (supercedes adhoc view arguments); unified put_thms/reset_thms;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-08-16 wenzelm 2005-08-16 added transfer; adapt local syntax to potential changes of theory syntax; added pretty_proof(_of);
2005-08-01 wenzelm 2005-08-01 Thm.full_prop_of;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify; tuned;
2005-07-19 wenzelm 2005-07-19 Inttab.defined;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-14 wenzelm 2005-07-14 sys_error;
2005-07-13 haftmann 2005-07-13 (fix for an accidental commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-07-01 wenzelm 2005-07-01 avoid polyeq;
2005-06-22 wenzelm 2005-06-22 removed proof data (see Pure/context.ML);
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection; tuned;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-09 wenzelm 2005-06-09 renamed extern to extern_thm; renamed cert/read_typ_raw to cert/read_typ_abbrev; added cert/read_typ_syntax; thms: NameSpace.table;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; support general naming context; added qualified_names, no_base_names, custom_accesses, restore_naming; removed qualified, restore_qualified; add_cases: RuleCases.T option; put_thms etc.: back to simple form, use naming context for extended functionality;
2005-05-22 wenzelm 2005-05-22 moved everything related to thms_containing to find_theorems.ML; export is_known; added fact_index_of, valid_thms; gen_read': removed unused dummies option; declare_term(_syntax): canonical argument order; removed declare_terms(_syntax);
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-17 wenzelm 2005-05-17 moved credit to CONTRIBUTORS; tuned;
2005-05-17 kleing 2005-05-17 use Drule.vars_of_terms
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-29 kleing 2005-04-29 credits
2005-04-29 kleing 2005-04-29 new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA)
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-17 wenzelm 2005-04-17 binds/thms: do not store options, but delete from table; tuned;
2005-04-16 wenzelm 2005-04-16 Syntax.mk_trfun;
2005-04-15 ballarin 2005-04-15 Removed most of the atp interface from Pure.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** added read_tyname/const;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.