2013-07-05 wenzelm [Fri, 05 Jul 2013 22:58:24 +0200] rev 52536
tuned signature;
tuned comments;
src/Pure/Isar/toplevel.ML src/Pure/PIDE/command.ML src/Pure/PIDE/command.scala src/Pure/PIDE/document.ML src/Pure/ROOT.ML

2013-07-05 wenzelm [Fri, 05 Jul 2013 22:09:16 +0200] rev 52535
tuned signature -- eliminated pointless type synonym;
src/Pure/PIDE/command.ML src/Pure/PIDE/command.scala src/Pure/Thy/thy_syntax.scala

2013-07-05 wenzelm [Fri, 05 Jul 2013 18:37:44 +0200] rev 52534
tuned signature;
tuned;
src/Pure/PIDE/command.ML src/Pure/PIDE/document.ML src/Pure/Thy/thy_load.ML

2013-07-05 wenzelm [Fri, 05 Jul 2013 17:09:28 +0200] rev 52533
clarified type Command.eval;
src/Pure/PIDE/command.ML src/Pure/PIDE/document.ML

2013-07-05 wenzelm [Fri, 05 Jul 2013 16:22:28 +0200] rev 52532
tuned signature;
src/Pure/PIDE/command.ML src/Pure/PIDE/document.ML

2013-07-05 wenzelm [Fri, 05 Jul 2013 16:01:45 +0200] rev 52531
tuned signature;
src/Pure/PIDE/command.scala src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.ML src/Pure/PIDE/document_id.scala src/Pure/PIDE/protocol.scala src/Pure/System/session.scala src/Tools/jEdit/src/active.scala

2013-07-05 wenzelm [Fri, 05 Jul 2013 15:38:03 +0200] rev 52530
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
src/Pure/Concurrent/synchronized.ML src/Pure/PIDE/command.ML src/Pure/PIDE/command.scala src/Pure/PIDE/document.ML src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.ML src/Pure/PIDE/document_id.scala src/Pure/PIDE/protocol.ML src/Pure/PIDE/protocol.scala src/Pure/ROOT src/Pure/ROOT.ML src/Pure/System/session.scala src/Pure/Thy/thy_syntax.scala src/Pure/build-jars src/Tools/jEdit/src/active.scala src/Tools/jEdit/src/pretty_text_area.scala src/Tools/jEdit/src/rendering.scala

2013-07-05 nipkow [Fri, 05 Jul 2013 16:45:31 +0200] rev 52529
improved proof automation for numerals
src/HOL/IMP/Hoare_Examples.thy src/HOL/IMP/Hoare_Total.thy

2013-07-05 wenzelm [Fri, 05 Jul 2013 14:09:06 +0200] rev 52528
merged

2013-07-04 wenzelm [Thu, 04 Jul 2013 23:51:47 +0200] rev 52527
separate exec_id assignment for Command.print states, without affecting result of eval;
tuned signature;
tuned;
src/Pure/Isar/toplevel.ML src/Pure/PIDE/command.ML src/Pure/PIDE/command.scala src/Pure/PIDE/document.ML src/Pure/PIDE/document.scala src/Pure/PIDE/protocol.ML src/Pure/PIDE/protocol.scala src/Tools/jEdit/src/pretty_text_area.scala