src/Pure/Isar/expression.ML
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.
2008-12-08 ballarin 2008-12-08 Explicitly close up defines.
2008-12-05 ballarin 2008-12-05 Interpretation in proof contexts.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-05 ballarin 2008-12-05 Merged.
2008-12-05 ballarin 2008-12-05 Interpretation in theories including interaction with subclass relation.
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-03 ballarin 2008-12-03 Sublocale: removed public after_qed; identifiers private to NewLocale.
2008-12-01 ballarin 2008-12-01 No resolution of patterns within context statements.
2008-11-28 ballarin 2008-11-28 Intro_locales_tac to simplify goals involving locale predicates.
2008-11-28 ballarin 2008-11-28 Ahere to modern naming conventions; proper treatment of internal vs external names.
2008-11-27 ballarin 2008-11-27 Proper treatment of expressions with free arguments.
2008-11-27 ballarin 2008-11-27 Sublocale command.
2008-11-25 ballarin 2008-11-25 Expression types cleaned up, proper treatment of term patterns.
2008-11-24 ballarin 2008-11-24 Read/cert_statement for theorem statements.
2008-11-21 ballarin 2008-11-21 add_locale functional.
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-20 ballarin 2008-11-20 Deleted debug message (PolyML).
2008-11-19 ballarin 2008-11-19 Type inference for elements through syntax module.
2008-11-18 ballarin 2008-11-18 Activate elements moved to element.ML.
2008-11-14 ballarin 2008-11-14 Initial part of locale reimplementation.
2008-10-28 haftmann 2008-10-28 making SMLNJ happy
2008-10-27 ballarin 2008-10-27 New-style locale expressions with instantiation (new file expression.ML).