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.
2004-06-21 ago added >>> : transition list -> unit;
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-12 ago added name_of, source_of, source;
2004-05-29 ago Output.timing;
2003-07-07 ago A patch by david aspinall
2002-08-08 ago exception SIMPROC_FAIL: solid error reporting of simprocs;
2002-02-28 ago use ignore_interrupt, raise_interrupt;
2002-02-12 ago ANTIQUOTE_FAIL;
2001-12-08 ago tuned print_state interfaces;
2001-11-28 ago added proof_to_theory';
2001-11-04 ago simplified Proof.init_state:
2001-10-31 ago Proof.init_state thy None;
2001-10-22 ago Display.current_goals_markers;
2000-10-25 ago tuned msg;
2000-08-03 ago added unknown_theory/proof/context;
2000-07-27 ago added enter_forward_proof;
2000-06-27 ago excursion_result: transform_error;
2000-06-26 ago tuned msg;
2000-06-25 ago excursion_result;
2000-05-31 ago Toplevel.no_timing;
2000-05-30 ago global timing flag;
2000-05-18 ago print_state: flag for proof only;
2000-05-05 ago GPLed;
2000-04-17 ago tuned msg;
2000-03-23 ago tuned output;
2000-03-15 ago eliminated toplevel stack;
1999-10-05 ago added is_toplevel;
1999-09-26 ago added keep', theory';
1999-09-25 ago avoid interrupts of read loop;