# 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