2004-12-10 aspinall [Fri, 10 Dec 2004 22:25:31 +0100] rev 15400
Insert pgmltext element into responses in PGIP mode
src/Pure/proof_general.ML

2004-12-10 berghofe [Fri, 10 Dec 2004 16:57:01 +0100] rev 15399
Added term cache to function condrew in order to speed up rewriting.
src/Pure/Proof/extraction.ML

2004-12-10 berghofe [Fri, 10 Dec 2004 16:55:58 +0100] rev 15398
- Exported functions new_name and new_names
- Fixed incompatible signatures problem in unfold_attr
src/Pure/codegen.ML

2004-12-10 berghofe [Fri, 10 Dec 2004 16:54:17 +0100] rev 15397
Fixed bug in mk_gen_of_def that could cause non-termination of the generator
for datatypes with nested recursion (such as trie).
src/HOL/Tools/datatype_codegen.ML

2004-12-10 berghofe [Fri, 10 Dec 2004 16:50:20 +0100] rev 15396
Preprocessors now transfer theorems to current theory in order to
avoid "incompatible signatures" exception.
src/HOL/Library/EfficientNat.thy

2004-12-10 berghofe [Fri, 10 Dec 2004 16:48:29 +0100] rev 15395
Moved code generator setup for product type to Product_Type.thy
src/HOL/Main.thy

2004-12-10 berghofe [Fri, 10 Dec 2004 16:48:01 +0100] rev 15394
New code generator for let and split.
src/HOL/Product_Type.thy

2004-12-10 berghofe [Fri, 10 Dec 2004 16:47:15 +0100] rev 15393
Realizer for exE now uses let instead of case.
src/HOL/Extraction.thy

2004-12-09 nipkow [Thu, 09 Dec 2004 18:30:59 +0100] rev 15392
First step in reorganizing Finite_Set
src/HOL/Equiv_Relations.thy src/HOL/Finite_Set.ML src/HOL/Finite_Set.thy src/HOL/List.thy src/HOL/Matrix/MatrixGeneral.thy src/HOL/NumberTheory/Euler.thy src/HOL/NumberTheory/EulerFermat.thy src/HOL/NumberTheory/Finite2.thy src/HOL/NumberTheory/Gauss.thy src/HOL/NumberTheory/Int2.thy src/HOL/NumberTheory/IntFact.thy src/HOL/NumberTheory/Quadratic_Reciprocity.thy src/HOL/NumberTheory/Residues.thy src/HOL/NumberTheory/WilsonBij.thy src/HOL/NumberTheory/WilsonRuss.thy

2004-12-09 paulson [Thu, 09 Dec 2004 16:45:46 +0100] rev 15391
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
TODO src/HOL/IsaMakefile src/HOL/Sum_Type.ML src/HOL/Sum_Type.thy src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/inductive_package.ML