2002-01-17 nipkow [Thu, 17 Jan 2002 19:32:22 +0100] rev 12792
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
src/HOL/Lex/RegExp.thy src/HOL/Lex/RegExp2NA.ML src/HOL/Lex/RegExp2NA.thy src/HOL/Lex/RegExp2NAe.ML src/HOL/Lex/RegExp2NAe.thy src/HOL/Lex/Scanner.thy

2002-01-17 kleing [Thu, 17 Jan 2002 15:06:36 +0100] rev 12791
registered directly executable version with the code generator
src/HOL/Library/While_Combinator.thy

2002-01-17 nipkow [Thu, 17 Jan 2002 12:58:31 +0100] rev 12790
*** empty log message ***
doc-src/TutorialI/tutorial.ind doc-src/TutorialI/tutorial.tex

2002-01-17 paulson [Thu, 17 Jan 2002 12:45:52 +0100] rev 12789
new definitions from Sidi Ehmety
src/ZF/Arith.ML src/ZF/List.ML src/ZF/List.thy src/ZF/Nat.thy

2002-01-17 paulson [Thu, 17 Jan 2002 12:45:36 +0100] rev 12788
made proofs more robust
src/ZF/AC/AC15_WO6.thy src/ZF/Induct/Ntree.thy

2002-01-17 paulson [Thu, 17 Jan 2002 10:35:59 +0100] rev 12787
mistakenly deleted this theory
src/ZF/AC/AC7_AC9.thy

2002-01-17 kleing [Thu, 17 Jan 2002 09:01:10 +0100] rev 12786
fixed
src/HOL/MicroJava/ROOT.ML

2002-01-16 wenzelm [Wed, 16 Jan 2002 23:19:34 +0100] rev 12785
GPLed;
src/Pure/Syntax/ROOT.ML src/Pure/Syntax/ast.ML src/Pure/Syntax/lexicon.ML src/Pure/Syntax/mixfix.ML src/Pure/Syntax/parser.ML src/Pure/Syntax/printer.ML src/Pure/Syntax/syn_ext.ML src/Pure/Syntax/syn_trans.ML src/Pure/Syntax/syntax.ML src/Pure/Syntax/token_trans.ML src/Pure/Syntax/type_ext.ML src/Pure/sign.ML src/Pure/theory.ML src/Pure/theory_data.ML

2002-01-16 wenzelm [Wed, 16 Jan 2002 23:18:20 +0100] rev 12784
added rewrite_term;
tuned;
GPLed;
src/Pure/pattern.ML

2002-01-16 wenzelm [Wed, 16 Jan 2002 23:17:44 +0100] rev 12783
interface to Pattern.rewrite_term;
src/Pure/meta_simplifier.ML