--- a/NEWS Thu Jan 19 21:22:26 2006 +0100
+++ b/NEWS Thu Jan 19 21:22:27 2006 +0100
@@ -361,6 +361,9 @@
Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
-- use plain ERROR instead.
+* ML/Isar: theory setup now has type (theory -> theory), instead of a
+list. INCOMPATIBILITY, may use #> to compose setup functions.
+
* Pure/Isar: Toplevel.theory_to_proof admits transactions that modify
the theory before entering a proof state. Transactions now always see
a quasi-functional intermediate checkpoint, both in interactive and