2006-11-11 ago level: do not account for local theory blocks (relevant for document preparation);
2006-11-10 ago simplified local theory wrappers;
2006-11-09 ago LocalTheory.restore;
2006-11-07 ago removed obsolete print_state_hook;
2006-11-04 ago removed checkpoint interface;
2006-10-12 ago renamed enter_forward_proof to enter_proof_body;
2006-10-11 ago exit_local_theory: pass interactive flag;
2006-10-11 ago added type global_theory -- theory or local_theory;
2006-10-09 ago loop: disallow exit in secure mode;
2006-10-07 ago TheoryTarget;
2006-09-21 ago member (op =);
2006-08-09 ago global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-07-14 ago keep/transaction: unified execution model (with debugging etc.);
2006-07-04 ago skip_proofs: do not skip proofs of schematic goals (warning);
2006-06-11 ago avoid unqualified exception;
2006-05-02 ago handle exception SYS_ERROR;
2006-02-17 ago checkpoint/copy_node: reset body context;
2006-02-15 ago added cases_node;
2006-02-06 ago added local_theory, with optional locale xname;
2006-01-27 ago swapped theory_context;
2006-01-19 ago keep: disable Output.toplevel_errors;
2006-01-14 ago sane ERROR vs. TOPLEVEL_ERROR handling;
2006-01-13 ago removed obsolete sign_of;
2006-01-10 ago added context_of -- generic context;
2006-01-06 ago transactions now always see quasi-functional intermediate checkpoint;
2006-01-05 ago hide type datatype node;
2006-01-04 ago added theory_to_theory_to_proof, which may change theory before entering the proof;
2006-01-04 ago tuned;
2005-10-18 ago simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-09-20 ago get_interrupt: special handling of now in ML-Systems/smlnj-basis-compat.ML;
2005-09-20 ago uniform handling of interrupts
2005-09-17 ago theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-16 ago catching exception Io
2005-09-13 ago added three_buffersN, print3;
2005-09-12 ago added interact flag to control mode of excursions;
2005-09-11 ago excursion: interactive if debug;
2005-09-05 ago added assert, command;
2005-08-31 ago added no_body_context;
2005-08-18 ago proof_to_theory_context: interaction flag;
2005-08-16 ago state: body context;
2005-07-13 ago added print_state_hook;
2005-07-06 ago debug: exception_trace;
2005-07-04 ago tuned;
2005-07-01 ago added profile flag;
2005-06-29 ago added print': print depending on print_mode;
2005-06-20 ago tuned;
2005-06-17 ago Context.DATA_FAIL;
2005-06-02 ago tuned msgs;
2005-05-23 ago node_trans: revert to original transaction code (pre 1.54);
2005-05-17 ago tuned;
2005-04-07 ago improved exn_message;
2005-03-26 ago new display of theory stamps
2005-03-10 ago Registrations of global locale interpretations: improved, better naming.
2005-03-09 ago First version of global registration command.
2005-03-03 ago Move towards standard functions.
2005-02-23 ago Modified node_trans to avoid duplication of signature stamps
2005-02-13 ago Deleted Library.option type.
2005-02-10 ago Toplevel.debug for debugging in Isar.
2005-01-11 ago excursion_result now also passes previous state to presentation functions.
2004-10-11 ago Some changes to allow skipping of proof scripts.