2014-11-12 immler [Wed, 12 Nov 2014 17:36:36 +0100] rev 58984
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
src/HOL/Transcendental.thy

2014-11-12 immler [Wed, 12 Nov 2014 17:36:32 +0100] rev 58983
cancel real of power of numeral also for equality and strict inequality;
simplify floor of power of numeral;
lemmas about real/floor
src/HOL/Real.thy

2014-11-12 immler [Wed, 12 Nov 2014 17:36:29 +0100] rev 58982
simplified computations based on round_up by reducing to round_down;
more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0
src/HOL/Decision_Procs/Approximation.thy src/HOL/Library/Float.thy

2014-11-12 immler [Wed, 12 Nov 2014 17:36:25 +0100] rev 58981
code equation for powr
src/HOL/Transcendental.thy

2014-11-11 wenzelm [Tue, 11 Nov 2014 21:14:19 +0100] rev 58980
merged

2014-11-11 wenzelm [Tue, 11 Nov 2014 20:11:38 +0100] rev 58979
more careful ML source positions, for improved PIDE markup;
src/Pure/Isar/attrib.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/method.ML src/Pure/ML/ml_context.ML

2014-11-11 wenzelm [Tue, 11 Nov 2014 18:16:25 +0100] rev 58978
more position information, e.g. relevant for errors in generated ML source;
src/Doc/antiquote_setup.ML src/HOL/ex/Cartouche_Examples.thy src/Pure/General/position.ML src/Pure/General/symbol_pos.ML src/Pure/Isar/attrib.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/method.ML src/Pure/Isar/token.ML src/Pure/ML/ml_antiquotations.ML src/Pure/ML/ml_context.ML src/Pure/ML/ml_file.ML src/Pure/ML/ml_lex.ML src/Pure/ML/ml_syntax.ML src/Pure/PIDE/markup.ML src/Pure/PIDE/markup.scala src/Pure/Syntax/syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Thy/latex.ML src/Pure/Thy/thy_output.ML src/Pure/Thy/thy_syntax.ML src/Pure/Tools/rail.ML

2014-11-11 wenzelm [Tue, 11 Nov 2014 15:55:31 +0100] rev 58977
more symbols;
src/CCL/CCL.thy src/CCL/Fix.thy src/CCL/Gfp.thy src/CCL/Hered.thy src/CCL/Lfp.thy src/CCL/Set.thy src/CCL/Term.thy src/CCL/Trancl.thy src/CCL/Type.thy src/CCL/Wfd.thy src/CCL/ex/Flag.thy src/CCL/ex/List.thy src/CCL/ex/Nat.thy src/CCL/ex/Stream.thy src/CTT/Arith.thy src/CTT/Bool.thy src/CTT/CTT.thy src/CTT/ex/Elimination.thy src/CTT/ex/Equality.thy src/CTT/ex/Synthesis.thy src/CTT/ex/Typechecking.thy src/LCF/LCF.thy src/LCF/ex/Ex1.thy src/LCF/ex/Ex2.thy src/LCF/ex/Ex3.thy src/LCF/ex/Ex4.thy

2014-11-11 wenzelm [Tue, 11 Nov 2014 13:50:56 +0100] rev 58976
tuned whitespace;
src/CCL/CCL.thy src/CCL/Term.thy src/CCL/Type.thy src/CCL/Wfd.thy src/CTT/Arith.thy src/CTT/CTT.thy src/CTT/ex/Typechecking.thy

2014-11-11 wenzelm [Tue, 11 Nov 2014 13:44:09 +0100] rev 58975
more markup;
src/CCL/CCL.thy src/CCL/Wfd.thy src/CTT/CTT.thy src/LCF/LCF.thy