# HG changeset patch
# User wenzelm
# Date 1005087024 -3600
# Node ID 4eb8061286e54fe124b4d47a7a7188dd9bcd71b8
# Parent  d46a32262bac7a58e58a137ef565c7ee23c3e984
* Isar/Pure: proper integration with ``locales''; unlike the original
version by Florian Kammueller, Isar locales package high-level proof
contexts rather than raw logical ones (e.g. we admit to include
attributes everywhere);
* Isar/Pure: theory goals now support ad-hoc contexts, which are
discharged in the result, as in ``lemma (assumes A and B) K: A .'';
syntax coincides with that of a locale body;

diff -r d46a32262bac -r 4eb8061286e5 NEWS
--- a/NEWS	Tue Nov 06 23:47:35 2001 +0100
+++ b/NEWS	Tue Nov 06 23:50:24 2001 +0100
@@ -62,6 +62,15 @@
 statements; NB: major inductive premises need to be put first, all the
 rest of the goal is passed through the induction;
 
+* Pure: proper integration with ``locales''; unlike the original
+version by Florian Kammueller, Isar locales package high-level proof
+contexts rather than raw logical ones (e.g. we admit to include
+attributes everywhere);
+
+* Pure: theory goals now support ad-hoc contexts, which are discharged
+in the result, as in ``lemma (assumes A and B) K: A .''; syntax
+coincides with that of a locale body;
+
 * Pure: renamed "antecedent" case to "rule_context";
 
 * Pure: added 'corollary' command;