diff -r cf47382db395 -r 23d0ffd48006 NEWS --- a/NEWS Fri Nov 07 16:22:25 2014 +0100 +++ b/NEWS Fri Nov 07 16:36:55 2014 +0100 @@ -18,6 +18,10 @@ structure in the body: 'oops' is no longer supported here. Minor INCOMPATIBILITY, use 'sorry' instead. +* Outer syntax commands are managed authentically within the theory +context, without implicit global state. Potential for accidental +INCOMPATIBILITY, make sure that required theories are really imported. + *** Prover IDE -- Isabelle/Scala/jEdit ***