2007-10-29 haftmann [Mon, 29 Oct 2007 16:46:22 +0100] rev 25228
added nbe
ANNOUNCE

2007-10-29 wenzelm [Mon, 29 Oct 2007 16:13:47 +0100] rev 25227
test_proof: do not change Proofterm.proofs here (not thread-safe);
src/Pure/Isar/proof.ML

2007-10-29 wenzelm [Mon, 29 Oct 2007 16:13:46 +0100] rev 25226
improved notion of 'nicer' fact names (observe some name space properties);
src/Pure/Isar/find_theorems.ML

2007-10-29 wenzelm [Mon, 29 Oct 2007 16:13:44 +0100] rev 25225
export is_hidden;
src/Pure/General/name_space.ML

2007-10-29 wenzelm [Mon, 29 Oct 2007 16:13:43 +0100] rev 25224
added bool_ord;
src/Pure/library.ML

2007-10-29 wenzelm [Mon, 29 Oct 2007 16:13:41 +0100] rev 25223
qualified Proofterm.proofs;
src/HOL/Main.thy src/HOL/Tools/datatype_realizer.ML src/Pure/ProofGeneral/ROOT.ML src/Pure/ProofGeneral/preferences.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/pure_setup.ML

2007-10-29 krauss [Mon, 29 Oct 2007 10:37:09 +0100] rev 25222
fun/function: generate case names for induction rules
src/HOL/NumberTheory/Fib.thy src/HOL/Tools/function_package/fundef_common.ML src/HOL/Tools/function_package/fundef_datatype.ML src/HOL/Tools/function_package/fundef_package.ML

2007-10-28 wenzelm [Sun, 28 Oct 2007 13:18:00 +0100] rev 25221
append/member: more light-weight way to declare authentic syntax;
tuned proofs;
src/HOL/List.thy

2007-10-28 wenzelm [Sun, 28 Oct 2007 13:16:09 +0100] rev 25220
made SML/NJ happy;
src/Tools/Compute_Oracle/am_sml.ML

2007-10-28 wenzelm [Sun, 28 Oct 2007 11:57:04 +0100] rev 25219
safe_exit: controlled_execution;
src/Pure/Isar/toplevel.ML