src/Pure/Isar/locale.ML
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 simplified ObjectLogic.atomize;
2007-06-19 wenzelm 2007-06-19 balanced conjunctions;
2007-06-03 wenzelm 2007-06-03 added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
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-04-23 wenzelm 2007-04-23 read_instantiations: proper type-inference with fixed variables, infer parameter types as well; gen_prep_registration: removed unused read_terms (dead code!); tuned;
2007-04-20 ballarin 2007-04-20 Interpretation equations applied to attributes; code cleanup in read_instantiations
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms; Syntax.mixfixT;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-04-13 ballarin 2007-04-13 Experimental interpretation code for definitions.
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2007-03-26 haftmann 2007-03-26 exported interface for intro rules
2007-02-23 haftmann 2007-02-23 locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
2007-02-19 schirmer 2007-02-19 more precise error message in parameter unification
2007-02-10 haftmann 2007-02-10 internal interfaces for interpretation and interpret
2007-02-04 wenzelm 2007-02-04 interpretation: attempt to be more serious about name_morphism;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 tuned print_locale output; add_decls: Thm.internalK;
2006-12-06 wenzelm 2006-12-06 export: added explicit term operation;
2006-12-05 wenzelm 2006-12-05 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
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.