src/Pure/Isar/locale.ML
2006-06-13 wenzelm 2006-06-13 use Drule.unvarify instead of obsolete Drule.freeze_all;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround; renaming: removed duplicate, use zip_options;
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.
2006-06-05 wenzelm 2006-06-05 export read/cert_expr; moved type witness to element.ML (abstract type); tuned;
2006-05-26 wenzelm 2006-05-26 activate Defines: fix frees;
2006-05-16 wenzelm 2006-05-16 replaced abbrevs by term_syntax, which is both simpler and more general;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 use conjunction stuff from conjunction.ML;
2006-04-08 wenzelm 2006-04-08 abbrevs: support print mode;
2006-03-20 wenzelm 2006-03-20 interpret: Proof.assert_forward_or_chain;
2006-03-20 ballarin 2006-03-20 Tuned signature of Locale.add_locale(_i).
2006-03-17 ballarin 2006-03-17 add_locale(_i) returns internal locale name.
2006-03-17 ballarin 2006-03-17 Internal restructuring: local parameters.
2006-03-16 ballarin 2006-03-16 New interface function parameters_of_expr.
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct; replaced qualified_force_prefix by qualified_names/sticky_prefix;
2006-02-12 wenzelm 2006-02-12 simplified TableFun.join;
2006-02-11 wenzelm 2006-02-11 added abbreviations: activated by init, no expressions yet;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list; tuned LocalDefs.cert_def;
2006-02-03 haftmann 2006-02-03 refined signature of locale module
2006-02-02 wenzelm 2006-02-02 Proof.refine_insert; statements: always use Attrib.src;
2006-02-02 wenzelm 2006-02-02 theorem(_in_locale): Element.statement, Obtain.statement;
2006-02-02 ballarin 2006-02-02 *_asms_of fixed.
2006-01-28 wenzelm 2006-01-28 LocalDefs;
2006-01-27 wenzelm 2006-01-27 init: include view; swapped Toplevel.theory_context; removed obsolete smart_note_thmss; moved note_thmss_qualified to PureThy; unified code of note_thmss(_i), add_thmss, locale_results;
2006-01-27 ballarin 2006-01-27 Interface to access the specification of a named locale.
2006-01-25 wenzelm 2006-01-25 turned abstract_term into ProofContext.abs_def; ProofContext.export_standard;
2006-01-24 wenzelm 2006-01-24 removed the_params;
2006-01-22 wenzelm 2006-01-22 added the_params;
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