src/Pure/Isar/locale.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 put_facts: do not pretend local thms were named;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes; mixfix: added Structure; tuned;
2006-01-07 wenzelm 2006-01-07 added init; tuned signature;
2006-01-04 haftmann 2006-01-04 fix: reintroduced pred_ctxt in gen_add_locale
2006-01-03 haftmann 2006-01-03 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
2006-01-03 wenzelm 2006-01-03 tuned;
2005-12-23 wenzelm 2005-12-23 Logic.mk_conjunction_list; PRECISE_CONJUNCTS: two levels;
2005-12-22 wenzelm 2005-12-22 CONJUNCTS2;
2005-12-21 haftmann 2005-12-21 discontinued unflat in favour of burrow and burrow_split
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
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-12-02 wenzelm 2005-12-02 defines: beta/eta contract lhs; replaced type_syntax by mixfix_type, which handles binders as well;
2005-12-02 haftmann 2005-12-02 introduced new map2, fold
2005-11-19 wenzelm 2005-11-19 CONJUNCTS;
2005-11-16 wenzelm 2005-11-16 tuned Pattern.match/unify; tuned fold;
2005-11-09 wenzelm 2005-11-09 moved datatype elem to element.ML; removed unused imports function;
2005-11-08 wenzelm 2005-11-08 avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;
2005-10-28 wenzelm 2005-10-28 tuned ProofContext.export interfaces;
2005-10-21 wenzelm 2005-10-21 Goal.prove_plain;
2005-10-18 wenzelm 2005-10-18 ObjectLogic.atomize_cterm;
2005-10-15 wenzelm 2005-10-15 goal statements: accomodate before_qed argument; ProofContext.note_thmss_i: natural argument order;
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-19 haftmann 2005-09-19 introduced AList module
2005-09-17 wenzelm 2005-09-17 interpretation: use goal commands without target -- no storing of results;
2005-09-16 ballarin 2005-09-16 tuned
2005-09-16 ballarin 2005-09-16 interpretation uses primitive goal interface
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 load late, after proof.ML; added goal commands: theorem, interpretation etc.; tuned some warnings -- single line only;
2005-09-09 ballarin 2005-09-09 fixed printing of locales
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-09-05 haftmann 2005-09-05 introduced binding priority 1 for linear combinators etc.
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-25 haftmann 2005-08-25 add_locale_context(_i) now exporting elements (still some refinements to be done)
2005-08-24 ballarin 2005-08-24 Interpretation in locales: extended back end; Printing of interpretations: option to show witness theorems;
2005-08-18 wenzelm 2005-08-18 added add_locale_context(_i), which returns the body context for presentation; note_thmss(_i), add_thmss: returns context for presentation; removed map_attrib_specs/facts (cf. Attrib.map_specs/facts);
2005-08-17 ballarin 2005-08-17 Improved generation of witnesses in interpretation.
2005-08-08 ballarin 2005-08-08 Release of interpretation in locale.
2005-08-02 ballarin 2005-08-02 First version of interpretation in locales. Not yet fully functional.
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify; Tactic.prove;
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-07 ballarin 2005-07-07 Preparations for interpretation of locales in locales.
2005-06-30 ballarin 2005-06-30 Proper treatment of beta-redexes in witness theorems.
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 NameSpace.extern_table; ProofContext.extern_thm;
2005-06-08 ballarin 2005-06-08 Fixed "axiom" generation for mixed locales with and without predicates.
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; Sign.declare_name replaces NameSpace.extend; proper use of naming context; tuned rename_facts; note_thmss_registrations: avoid non-linear use of thy (via sign);
2005-05-27 ballarin 2005-05-27 SML/NJ compatibility.
2005-05-27 ballarin 2005-05-27 Deleted old code.