2006-01-14 wenzelm [Sat, 14 Jan 2006 22:25:34 +0100] rev 18688
generic attributes;
src/HOL/Tools/datatype_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/record_package.ML src/HOLCF/domain/theorems.ML src/HOLCF/fixrec_package.ML src/Provers/clasimp.ML src/Provers/classical.ML src/Provers/splitter.ML src/Pure/simplifier.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/primrec_package.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:20:51 +0100] rev 18687
tuned;
NEWS

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:15:24 +0100] rev 18686
* ML/Isar: simplified treatment of user-level errors;
NEWS

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:18 +0100] rev 18685
sane ERROR vs. TOPLEVEL_ERROR handling;
added program;
src/Pure/Isar/toplevel.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:17 +0100] rev 18684
added Isar.toplevel;
src/Pure/Isar/outer_syntax.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:16 +0100] rev 18683
Output.error_msg;
src/Pure/General/scan.ML src/Pure/Isar/session.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:15 +0100] rev 18682
removed special ERROR handling stuff (transform_error etc.);
moved plain ERROR/error to library.ML;
added toplevel_errors, exception TOPLEVEL_ERROR;
error_msg, panic, info, debug no longer pervasive;
src/Pure/General/output.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:14 +0100] rev 18681
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
added transform_failure;
added prefix;
src/Pure/library.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:13 +0100] rev 18680
Output.debug;
src/HOL/Tools/ATP/watcher.ML src/HOL/Tools/meson.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML

2006-01-14 wenzelm [Sat, 14 Jan 2006 17:14:11 +0100] rev 18679
generated code: raise Match instead of ERROR;
src/HOL/MicroJava/J/JListExample.thy src/HOL/MicroJava/JVM/JVMListExample.thy src/Pure/codegen.ML