src/Pure/Isar/locale.ML
2006-11-30 wenzelm 2006-11-30 Goal.norm/close_result;
2006-11-29 wenzelm 2006-11-29 *** bad commit -- reverted to previous version ***
2006-11-29 wenzelm 2006-11-29 simplified add_thmss; mark predicate definitions as internal;
2006-11-29 wenzelm 2006-11-29 simplified add_thmss; mark predicate definitions as internal;
2006-11-26 wenzelm 2006-11-26 Element.map_ctxt_attrib;
2006-11-24 wenzelm 2006-11-24 tuned morphisms;
2006-11-23 wenzelm 2006-11-23 uniform interface for type_syntax/term_syntax/declaration, dependent on morphism; tuned some morphisms;
2006-11-23 wenzelm 2006-11-23 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
2006-11-21 wenzelm 2006-11-21 notes: proper kind; simplified Proof.theorem(_i); context_statement: ProofContext.set_stmt after import;
2006-11-15 wenzelm 2006-11-15 add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
2006-11-14 wenzelm 2006-11-14 replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
2006-11-14 wenzelm 2006-11-14 simplified Proof.theorem(_i) interface; simplified goal kind output;
2006-11-09 wenzelm 2006-11-09 removed obsolete locale_results;
2006-11-07 wenzelm 2006-11-07 removed obsolete theorem statements (cf. specification.ML);
2006-11-07 schirmer 2006-11-07 exported intro_locales_tac ----------------------------------------------------------------------
2006-10-14 wenzelm 2006-10-14 export map_elem; added read_context_statement_i (internal locale name);
2006-10-12 wenzelm 2006-10-12 interpretation_in_locale: standalone goal setup; moved theorem statements to bottom;
2006-10-11 wenzelm 2006-10-11 add_locale(_i): return actual result context; cert_facts: allow qualified names;
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 wenzelm 2006-10-09 removed obsolete note_thmss(_i); simplified add_thmss; tuned;
2006-10-07 wenzelm 2006-10-07 tuned;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory); theorem/interpretation: slightly more uniform treatment of after_qeds; theorem conclusion: proper fix_frees;
2006-08-03 ballarin 2006-08-03 Updated comments.
2006-08-02 wenzelm 2006-08-02 removed obsolete Drule.frees/vars_of etc.; simplified Assumption/ProofContext.export;
2006-07-27 wenzelm 2006-07-27 renamed ProofContext.fix_frees to Variable.fix_frees;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-25 wenzelm 2006-07-25 renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
2006-07-19 ballarin 2006-07-19 Strict dfs traversal of imported and registered identifiers.
2006-07-11 wenzelm 2006-07-11 Name.internal; Name.invent_list;
2006-07-11 ballarin 2006-07-11 Witness theorems of interpretations now transfered to current theory.
2006-07-08 wenzelm 2006-07-08 Element.prove_witness: context; Goal.prove_global;
2006-07-07 ballarin 2006-07-07 Fixed erroneous check-in.
2006-07-07 ballarin 2006-07-07 Internal restructuring: identify no longer computes syntax.
2006-07-06 wenzelm 2006-07-06 removed obsolete locale view;
2006-07-04 ballarin 2006-07-04 Locales no longer generate views. The following functions have changed signatures: Locale.init, Locale.add_thmss, Locale.read/cert_context_statement.
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-22 ballarin 2006-06-22 Improved handling of defines imported in duplicate.
2006-06-20 haftmann 2006-06-20 fixed sml/nj value restriction problem
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-17 wenzelm 2006-06-17 Variable.importT_inst; Term.internal;
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable; tuned;
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;