src/Pure/Isar/expression.ML
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-05 haftmann 2010-05-05 eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-15 wenzelm 2010-03-15 replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-19 wenzelm 2010-02-19 Thm.def_binding;
2010-02-18 wenzelm 2010-02-18 locale: more precise treatment of naming vs. binding;
2010-02-16 wenzelm 2010-02-16 comment;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-12 wenzelm 2009-11-12 eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-10-30 haftmann 2009-10-30 tuned variable names of bindings; conceal predicate constants
2009-10-29 wenzelm 2009-10-29 eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-01 ballarin 2009-10-01 Merged.
2009-10-01 ballarin 2009-10-01 Avoid administrative overhead for identity mixins.
2009-10-01 wenzelm 2009-10-01 merged
2009-10-01 ballarin 2009-10-01 Merged.
2009-09-29 ballarin 2009-09-29 Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-19 ballarin 2009-09-19 Explicit management of registration mixins.
2009-08-19 ballarin 2009-08-19 Improved comments and api names.
2009-09-30 wenzelm 2009-09-30 eliminated redundant parameters;
2009-09-03 haftmann 2009-09-03 proper class syntax for sublocale class < expr
2009-07-15 haftmann 2009-07-15 simplification of locale interfaces
2009-07-10 haftmann 2009-07-10 merged
2009-07-10 haftmann 2009-07-10 tuned locale interface
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-03-30 wenzelm 2009-03-30 prep_full_context_statement: explicit record of flags; prep_declaration (for add_locale): disallow autofixed frees;
2009-03-29 wenzelm 2009-03-29 merged
2009-03-29 ballarin 2009-03-29 Merged.
2009-03-29 ballarin 2009-03-29 Normalise equation only for morphism, not thm stored in theory.
2009-03-29 wenzelm 2009-03-29 tuned;
2009-03-29 wenzelm 2009-03-29 simplified Element.activate(_i): singleton version;
2009-03-29 wenzelm 2009-03-29 tuned;
2009-03-29 wenzelm 2009-03-29 unified binding prefix terminology;
2009-03-28 wenzelm 2009-03-28 simplified Locale.activate operations, using generic context; misc tuning;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
2009-03-28 wenzelm 2009-03-28 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-26 wenzelm 2009-03-26 register_locale: produce stamps at the spot where elements are registered; tuned signature; misc internal tuning and simplification;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-12 wenzelm 2009-03-12 renamed sticky_prefix to mandatory_path;
2009-03-12 wenzelm 2009-03-12 replaced old-style add_path/no_base_names by sticky_prefix;
2009-03-11 wenzelm 2009-03-11 Thm.def_binding_optional;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-07 wenzelm 2009-03-07 Binding.str_of: removed verbose feature, include qualifier in output; renamed Binding.add_prefix to Binding.prefix;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
2009-03-03 wenzelm 2009-03-03 Binding.str_of; removed dead code; tuned;
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-02-03 haftmann 2009-02-03 handling type classes without parameters