# HG changeset patch
# User wenzelm
# Date 1137702147 -3600
# Node ID 0888eca0f1be41fd44f7d5accae3cf48d590acc4
# Parent  54693225c2f45e132ba3e9753017e87adc9f96ab
* ML/Isar: theory setup has type (theory -> theory);

diff -r 54693225c2f4 -r 0888eca0f1be NEWS
--- 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