2013-03-29 wenzelm [Fri, 29 Mar 2013 22:14:27 +0100] rev 51580
Pretty.item markup for improved readability of lists of items;
src/HOL/Tools/inductive.ML src/Provers/classical.ML src/Pure/Isar/calculation.ML src/Pure/Isar/code.ML src/Pure/Isar/context_rules.ML src/Pure/Syntax/syntax.ML src/Pure/simplifier.ML src/Tools/induct.ML

2013-03-29 wenzelm [Fri, 29 Mar 2013 22:13:02 +0100] rev 51579
tuned message;
src/HOL/Orderings.thy

2013-03-29 haftmann [Fri, 29 Mar 2013 11:32:07 +0100] rev 51578
convenience check for vain instantiation
src/Pure/Isar/class.ML

2013-03-29 wenzelm [Fri, 29 Mar 2013 13:32:53 +0100] rev 51577
improved centering via strikethrough offset;
src/Tools/jEdit/src/rich_text_area.scala

2013-03-28 boehmes [Thu, 28 Mar 2013 23:44:43 +0100] rev 51576
re-generated SMT certificates
src/HOL/Boogie/Examples/Boogie_Max.certs src/HOL/Boogie/Examples/VCC_Max.certs src/HOL/SMT_Examples/SMT_Examples.certs

2013-03-28 boehmes [Thu, 28 Mar 2013 23:44:41 +0100] rev 51575
new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code
src/HOL/ATP.thy src/HOL/Tools/Metis/metis_generate.ML src/HOL/Tools/SMT/smt_config.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML src/HOL/Tools/legacy_monomorph.ML src/HOL/Tools/monomorph.ML

2013-03-28 wenzelm [Thu, 28 Mar 2013 22:42:18 +0100] rev 51574
ghost bullet via markup, which is painted as bar under text (normally space);
src/Pure/General/pretty.scala src/Pure/PIDE/markup.scala src/Tools/jEdit/etc/options src/Tools/jEdit/src/rendering.scala src/Tools/jEdit/src/rich_text_area.scala

2013-03-28 kleing [Thu, 28 Mar 2013 16:11:48 +0100] rev 51573
replace induction by hammer
src/HOL/IMP/Fold.thy

2013-03-28 wenzelm [Thu, 28 Mar 2013 15:47:03 +0100] rev 51572
merged

2013-03-28 wenzelm [Thu, 28 Mar 2013 15:37:39 +0100] rev 51571
merged;