src/Pure/Isar/expression.ML
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
2009-02-01 haftmann 2009-02-01 proper declared constants in class expressions
2009-01-21 wenzelm 2009-01-21 eliminated obsolete var morphism; tuned;
2009-01-21 haftmann 2009-01-21 refined witness algebra
2009-01-19 haftmann 2009-01-19 tuned
2009-01-17 haftmann 2009-01-17 explicit equation morphism
2009-01-16 haftmann 2009-01-16 corrected preparation of instances: parameters are proper names, not raw terms
2009-01-16 haftmann 2009-01-16 added cert_read_declaration; more exports; tuned signature
2009-01-15 haftmann 2009-01-15 tuned interpretation code
2009-01-11 haftmann 2009-01-11 explicit bookkeeping of intro rules and axiom
2009-01-07 haftmann 2009-01-07 merged
2009-01-07 haftmann 2009-01-07 tuned signature; changed locale predicate name convention
2009-01-07 wenzelm 2009-01-07 qed/after_qed: singleton result;
2009-01-06 haftmann 2009-01-06 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 rearranged target theories
2009-01-01 wenzelm 2009-01-01 avoid polymorphic equality;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-12-30 wenzelm 2008-12-30 prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;
2008-12-23 ballarin 2008-12-23 More liberal consistency check for defines elements.
2008-12-19 ballarin 2008-12-19 Merged.
2008-12-18 Norbert Schirmer 2008-12-18 adapted statespace module to new locales;
2008-12-19 ballarin 2008-12-19 Intro_locales_tac knows about defines elements; more robust export morphism.
2008-12-18 ballarin 2008-12-18 Merged.
2008-12-17 ballarin 2008-12-17 Prevent defines from being checked in interpretation.
2008-12-18 ballarin 2008-12-18 Refactored: evaluate specification text only in locale declarations.
2008-12-16 ballarin 2008-12-16 Finer-grained activation so that facts from earlier elements are available.
2008-12-16 ballarin 2008-12-16 Use correct mode when parsing elements and conclusion.
2008-12-14 ballarin 2008-12-14 Strict prefixes in locales expressions.
2008-12-12 ballarin 2008-12-12 Equations in interpretation as goals.
2008-12-11 ballarin 2008-12-11 Interpretation in theories: first version with equations.
2008-12-10 ballarin 2008-12-10 Use prefix component of bindings for locale prefixes.
2008-12-10 ballarin 2008-12-10 Preserve idents (expression in sublocale).
2008-12-10 ballarin 2008-12-10 Satisfy a_axioms.
2008-12-10 ballarin 2008-12-10 Merged.
2008-12-10 ballarin 2008-12-10 Enable keyword 'structure' in for clause of locale expression.
2008-12-09 ballarin 2008-12-09 Correct order of defines in specification.
2008-12-09 ballarin 2008-12-09 Pass on defines in inheritance; reject illicit defines created by instantiation.
2008-12-09 ballarin 2008-12-09 Order of implicit parameters in locale expression.
2008-12-09 ballarin 2008-12-09 When adding locales, delay notes until local theory is built.
2008-12-08 ballarin 2008-12-08 Default names for definitions.
2008-12-08 ballarin 2008-12-08 Proper shape of assumptions generated from Defines elements.
2008-12-08 ballarin 2008-12-08 Merged.