2011-07-10 haftmann [Sun, 10 Jul 2011 14:26:07 +0200] rev 43740
more succinct proofs
src/HOL/Complete_Lattice.thy

2011-07-10 haftmann [Sun, 10 Jul 2011 14:14:19 +0200] rev 43739
more succinct proofs
src/HOL/Complete_Lattice.thy

2011-07-10 bulwahn [Sun, 10 Jul 2011 19:33:27 +0200] rev 43738
adding a very liberal timeout for values after a test case failed due to the restricted timeout
src/HOL/IMP/C_like.thy

2011-07-10 bulwahn [Sun, 10 Jul 2011 14:02:27 +0200] rev 43737
improved NEWS
NEWS

2011-07-09 bulwahn [Sat, 09 Jul 2011 21:18:20 +0200] rev 43736
NEWS
NEWS

2011-07-09 bulwahn [Sat, 09 Jul 2011 21:09:09 +0200] rev 43735
standardized String.concat towards implode (cf. c37a1f29bbc0)
src/HOL/Tools/Predicate_Compile/code_prolog.ML

2011-07-09 bulwahn [Sat, 09 Jul 2011 19:29:25 +0200] rev 43734
adding quickcheck examples for evaluating floor and ceiling functions
src/HOL/ex/Quickcheck_Examples.thy

2011-07-09 bulwahn [Sat, 09 Jul 2011 19:28:33 +0200] rev 43733
adding code equations to execute floor and ceiling on rational and real numbers
src/HOL/Archimedean_Field.thy src/HOL/Rat.thy src/HOL/RealDef.thy

2011-07-09 bulwahn [Sat, 09 Jul 2011 13:41:58 +0200] rev 43732
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
src/HOL/Archimedean_Field.thy src/HOL/Rat.thy src/HOL/RealDef.thy

2011-07-10 wenzelm [Sun, 10 Jul 2011 20:59:04 +0200] rev 43731
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
tuned signature;
NEWS src/Pure/General/xml_data.ML src/Pure/General/xml_data.scala src/Pure/General/yxml.ML src/Pure/Isar/token.ML src/Pure/PIDE/isar_document.ML src/Pure/PIDE/isar_document.scala src/Pure/Syntax/syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Thy/thy_header.scala src/Pure/Tools/find_theorems.ML src/Pure/term.scala src/Pure/term_xml.ML