2008-11-29 nipkow [Sat, 29 Nov 2008 13:39:45 +0100] rev 28906
Floats for Real.
src/HOL/Real/RealDef.thy src/HOL/Real/RealPow.thy src/HOL/Real/float_syntax.ML

2008-11-29 nipkow [Sat, 29 Nov 2008 13:39:23 +0100] rev 28905
new file float_syntax.ML
src/HOL/IsaMakefile

2008-11-29 nipkow [Sat, 29 Nov 2008 13:37:13 +0100] rev 28904
New lexical item "float".
src/Pure/General/markup.ML src/Pure/Syntax/lexicon.ML src/Pure/Syntax/syn_ext.ML src/Pure/Syntax/syntax.ML src/Pure/pure_thy.ML

2008-11-28 ballarin [Fri, 28 Nov 2008 17:43:06 +0100] rev 28903
Intro_locales_tac to simplify goals involving locale predicates.
src/FOL/ex/NewLocaleTest.thy src/Pure/Isar/expression.ML src/Pure/Isar/new_locale.ML

2008-11-28 ballarin [Fri, 28 Nov 2008 12:26:14 +0100] rev 28902
Ahere to modern naming conventions; proper treatment of internal vs external names.
src/FOL/ex/NewLocaleSetup.thy src/Pure/Isar/expression.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/new_locale.ML

2008-11-28 kleing [Fri, 28 Nov 2008 11:55:46 +0100] rev 28901
added Tim's find_theorems performance patch
CONTRIBUTORS

2008-11-28 kleing [Fri, 28 Nov 2008 11:37:20 +0100] rev 28900
FindTheorems performance improvements (from Timothy Bourke)

* Prefilter the list of theorems based on the constants and
free variables in Pattern search terms, before calling
Pattern.matches_subterm.
* Apply filters successively rather than running each and
then finding the intersection.
* Show the time taken to run a query.
src/Pure/Isar/find_theorems.ML

2008-11-28 ballarin [Fri, 28 Nov 2008 11:14:13 +0100] rev 28899
Perform higher-order pattern matching during round-up.
src/FOL/ex/NewLocaleTest.thy src/Pure/Isar/new_locale.ML

2008-11-27 ballarin [Thu, 27 Nov 2008 21:25:34 +0100] rev 28898
Proper treatment of expressions with free arguments.
src/FOL/ex/NewLocaleTest.thy src/Pure/Isar/expression.ML

2008-11-27 ballarin [Thu, 27 Nov 2008 21:25:16 +0100] rev 28897
Roundup bound.
src/Pure/Isar/new_locale.ML