2012-08-21 wenzelm [Tue, 21 Aug 2012 12:15:25 +0200] rev 48870
clarified initialization of Thy_Load, Thy_Info, Session;
src/Pure/Isar/outer_syntax.scala src/Pure/System/build.scala src/Pure/System/session.scala src/Pure/Thy/thy_info.scala src/Pure/Thy/thy_load.scala src/Tools/jEdit/src/jedit_thy_load.scala src/Tools/jEdit/src/plugin.scala src/Tools/jEdit/src/session_dockable.scala

2012-08-21 wenzelm [Tue, 21 Aug 2012 11:00:54 +0200] rev 48869
tuned;
src/Pure/Thy/thy_load.ML

2012-08-20 wenzelm [Mon, 20 Aug 2012 21:52:31 +0200] rev 48868
more robust cleaning of "% tag" and "-- cmt";
src/Pure/Thy/thy_load.ML

2012-08-20 wenzelm [Mon, 20 Aug 2012 17:05:53 +0200] rev 48867
some support for inlining file content into outer syntax token language;
etc/isar-keywords-ZF.el etc/isar-keywords.el src/Pure/Isar/keyword.ML src/Pure/Isar/keyword.scala src/Pure/Isar/token.ML src/Pure/ROOT.ML src/Pure/System/build.scala src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_syntax.ML

2012-08-20 wenzelm [Mon, 20 Aug 2012 15:43:10 +0200] rev 48866
tuned comment;
src/Pure/General/path.ML

2012-08-20 wenzelm [Mon, 20 Aug 2012 14:23:20 +0200] rev 48865
tuned;
src/Pure/Thy/thy_syntax.ML

2012-08-20 wenzelm [Mon, 20 Aug 2012 14:09:09 +0200] rev 48864
added keyword kind "thy_load" (with optional list of file extensions);
lib/scripts/keywords src/Pure/Isar/keyword.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/outer_syntax.scala src/Pure/ML/ml_antiquote.ML src/Pure/PIDE/protocol.ML src/Pure/PIDE/protocol.scala src/Pure/ProofGeneral/pgip_parser.ML src/Pure/System/build.scala src/Pure/Thy/thy_header.ML src/Pure/Thy/thy_header.scala

2012-08-20 wenzelm [Mon, 20 Aug 2012 13:58:06 +0200] rev 48863
updated generated files;
doc-src/Codegen/Thy/document/Introduction.tex doc-src/Codegen/Thy/document/Refinement.tex doc-src/Codegen/Thy/examples/example.ML

2012-08-20 wenzelm [Mon, 20 Aug 2012 13:39:41 +0200] rev 48862
more strict syntax, according to manual;
src/Pure/System/build.scala

2012-08-20 nipkow [Mon, 20 Aug 2012 08:40:18 +0200] rev 48861
abstracted lemma
src/HOL/Big_Operators.thy