2008-02-18 huffman [Mon, 18 Feb 2008 02:10:55 +0100] rev 26089
proved linorder and wellorder class instances
src/HOL/Library/Nat_Infinity.thy

2008-02-17 wenzelm [Sun, 17 Feb 2008 19:04:50 +0100] rev 26088
added get_parent (for AWE);
tuned;
src/HOL/Tools/record_package.ML

2008-02-17 wenzelm [Sun, 17 Feb 2008 18:43:17 +0100] rev 26087
added perl wrapper for robust signal handling;
src/Pure/General/system_process.ML

2008-02-17 huffman [Sun, 17 Feb 2008 06:49:53 +0100] rev 26086
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
NEWS src/HOL/Groebner_Basis.thy src/HOL/Import/HOL/HOL4Prob.thy src/HOL/Import/HOL/HOL4Real.thy src/HOL/Import/HOL/HOL4Vec.thy src/HOL/Import/HOL/HOL4Word32.thy src/HOL/Int.thy src/HOL/IntDiv.thy src/HOL/Library/Char_nat.thy src/HOL/Library/Code_Index.thy src/HOL/Library/Code_Integer.thy src/HOL/Library/Word.thy src/HOL/NatBin.thy src/HOL/NumberTheory/Euler.thy src/HOL/Presburger.thy src/HOL/Real/Float.thy src/HOL/Tools/ComputeNumeral.thy src/HOL/Tools/Qelim/cooper_data.ML src/HOL/Tools/numeral.ML src/HOL/Tools/numeral_syntax.ML src/HOL/Word/BinBoolList.thy src/HOL/Word/BinGeneral.thy src/HOL/Word/BinOperations.thy src/HOL/Word/BitSyntax.thy src/HOL/Word/Examples/WordExamples.thy src/HOL/Word/Num_Lemmas.thy src/HOL/Word/WordArith.thy src/HOL/Word/WordMain.thy src/HOL/Word/WordShift.thy src/HOL/hologic.ML src/HOL/int_arith1.ML src/HOL/int_factor_simprocs.ML src/Tools/code/code_target.ML

2008-02-16 wenzelm [Sat, 16 Feb 2008 16:52:09 +0100] rev 26085
removed spurious PolyML.makestring;
src/Pure/General/system_process.ML

2008-02-16 wenzelm [Sat, 16 Feb 2008 16:44:02 +0100] rev 26084
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
src/Pure/ML-Systems/alice.ML src/Pure/ML-Systems/mosml.ML src/Pure/ML-Systems/polyml.ML src/Pure/ML-Systems/poplogml.ML src/Pure/ML-Systems/smlnj.ML

2008-02-16 wenzelm [Sat, 16 Feb 2008 16:44:02 +0100] rev 26083
removed managed_process (cf. General/shell_process.ML);
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
tuned timeLimit: sleep already interruptible by default;
schedule: restore attributes of body, instead of forcing interruptible execution;
src/Pure/ML-Systems/multithreading_polyml.ML

2008-02-16 wenzelm [Sat, 16 Feb 2008 16:44:00 +0100] rev 26082
removed managed_process (cf. General/shell_process.ML);
src/Pure/ML-Systems/multithreading.ML

2008-02-16 wenzelm [Sat, 16 Feb 2008 16:43:59 +0100] rev 26081
exn_message: added TimeLimit.TimeOut;
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
src/Pure/Isar/toplevel.ML

2008-02-16 wenzelm [Sat, 16 Feb 2008 16:43:57 +0100] rev 26080
export deny_secure;
src/Pure/General/secure.ML