2014-05-21 desharna [Wed, 21 May 2014 18:55:34 +0200] rev 57046
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

2014-05-21 wenzelm [Wed, 21 May 2014 16:46:14 +0200] rev 57045
merged

2014-05-21 wenzelm [Wed, 21 May 2014 16:21:11 +0200] rev 57044
more uniform Font_Info.Zoom_Box;
misc tuning and clarification;
src/Pure/GUI/gui.scala src/Tools/Graphview/src/graph_panel.scala src/Tools/Graphview/src/main_panel.scala src/Tools/jEdit/src/font_info.scala src/Tools/jEdit/src/info_dockable.scala src/Tools/jEdit/src/output_dockable.scala src/Tools/jEdit/src/query_dockable.scala src/Tools/jEdit/src/simplifier_trace_window.scala src/Tools/jEdit/src/sledgehammer_dockable.scala

2014-05-21 wenzelm [Wed, 21 May 2014 15:24:42 +0200] rev 57043
added zoom box, like for outer output windows;
src/Tools/jEdit/src/simplifier_trace_window.scala

2014-05-21 wenzelm [Wed, 21 May 2014 14:42:45 +0200] rev 57042
tuned signature;
src/Tools/jEdit/src/info_dockable.scala src/Tools/jEdit/src/output_dockable.scala src/Tools/jEdit/src/pretty_text_area.scala src/Tools/jEdit/src/query_dockable.scala src/Tools/jEdit/src/simplifier_trace_window.scala

2014-05-21 Lars Hupel <lars.hupel@mytum.de> [Wed, 21 May 2014 16:26:04 +0200] rev 57041
consolidate "break_thm" and "break_term" attributes into "simp_break";
src/Pure/Tools/simplifier_trace.ML

2014-05-21 blanchet [Wed, 21 May 2014 14:09:43 +0200] rev 57040
docs
src/Doc/Nitpick/document/root.tex src/Doc/Sledgehammer/document/root.tex

2014-05-21 blanchet [Wed, 21 May 2014 14:09:43 +0200] rev 57039
added comment
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

2014-05-21 blanchet [Wed, 21 May 2014 14:09:42 +0200] rev 57038
move exhaust first, for technical reasons
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2014-05-21 blanchet [Wed, 21 May 2014 14:09:42 +0200] rev 57037
avoid markup-generating @{make_string}
src/HOL/Tools/Sledgehammer/sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML