2009-12-22 wenzelm [Tue, 22 Dec 2009 15:00:43 +0100] rev 34159
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
src/Pure/IsaMakefile src/Pure/Isar/outer_parse.scala

2009-12-22 wenzelm [Tue, 22 Dec 2009 15:00:03 +0100] rev 34158
class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;
src/Pure/Isar/outer_keyword.scala

2009-12-22 wenzelm [Tue, 22 Dec 2009 14:58:13 +0100] rev 34157
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
added Token_Reader;
tuned;
src/Pure/General/scan.scala src/Pure/Isar/outer_lex.scala

2009-12-21 paulson [Mon, 21 Dec 2009 16:50:28 +0000] rev 34156
Changes in generated code, apparently caused by changes to the code generation system itself.
doc-src/Codegen/Thy/examples/Example.hs doc-src/Codegen/Thy/examples/example.ML

2009-12-21 paulson [Mon, 21 Dec 2009 16:49:04 +0000] rev 34155
Polishing up the English
doc-src/Codegen/Thy/Adaptation.thy doc-src/Codegen/Thy/Further.thy doc-src/Codegen/Thy/Introduction.thy doc-src/Codegen/Thy/Program.thy doc-src/Codegen/Thy/document/Adaptation.tex doc-src/Codegen/Thy/document/Further.tex doc-src/Codegen/Thy/document/Introduction.tex doc-src/Codegen/Thy/document/Program.tex

2009-12-21 wenzelm [Mon, 21 Dec 2009 10:40:14 +0100] rev 34154
merged
src/Pure/ML-Systems/exn.ML

2009-12-21 haftmann [Mon, 21 Dec 2009 08:32:22 +0100] rev 34153
merged
src/HOL/Fun.thy

2009-12-21 haftmann [Mon, 21 Dec 2009 08:32:04 +0100] rev 34152
clarified various user-defined syntax issues
src/Tools/Code/code_printer.ML src/Tools/Code/code_target.ML

2009-12-21 haftmann [Mon, 21 Dec 2009 08:32:04 +0100] rev 34151
prefer prefix "iso" over potentially misleading "is"; tuned
src/HOL/Record.thy src/HOL/Tools/record.ML

2009-12-21 haftmann [Mon, 21 Dec 2009 08:32:03 +0100] rev 34150
moved lemmas o_eq_dest, o_eq_elim here
src/HOL/Fun.thy