2013-07-03 wenzelm [Wed, 03 Jul 2013 22:30:33 +0200] rev 52515
more print function parameters;
check command_visible statically in assignment, instead of dynamically in execution;
src/Pure/PIDE/command.ML src/Pure/PIDE/document.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 21:55:15 +0200] rev 52514
tuned;
src/Pure/PIDE/document.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 21:38:10 +0200] rev 52513
discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
src/Pure/PIDE/document.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 21:32:58 +0200] rev 52512
tuned;
src/Pure/PIDE/document.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 17:50:47 +0200] rev 52511
allow multiple print functions;
src/Pure/PIDE/command.ML src/Pure/PIDE/document.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 16:58:35 +0200] rev 52510
tuned signature;
src/Pure/Isar/outer_syntax.ML src/Pure/PIDE/command.ML src/Pure/PIDE/document.ML src/Pure/ROOT.ML src/Pure/Thy/thy_load.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 16:19:57 +0200] rev 52509
tuned signature;
src/Pure/Isar/outer_syntax.ML src/Pure/PIDE/command.ML src/Pure/PIDE/command.scala src/Pure/PIDE/document.ML

2013-07-03 wenzelm [Wed, 03 Jul 2013 15:19:36 +0200] rev 52508
tuned;
src/Pure/PIDE/document.ML src/Pure/PIDE/document.scala

2013-07-03 wenzelm [Wed, 03 Jul 2013 15:11:15 +0200] rev 52507
tuned signature;
src/Pure/General/symbol.scala src/Pure/PIDE/command.scala

2013-07-03 traytel [Wed, 03 Jul 2013 20:41:41 +0200] rev 52506
use long goal format in rel_induct theorem
src/HOL/BNF/Tools/bnf_fp_util.ML src/HOL/BNF/Tools/bnf_gfp_tactics.ML src/HOL/BNF/Tools/bnf_lfp_tactics.ML