- New theories Lambda/NormalForm and Lambda/Standardization
- Integrated Executable_Rat and Executable_Real theories into
Rational and RealDef theories

--- a/src/HOL/IsaMakefile	Thu Sep 06 11:50:32 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 06 11:52:13 2007 +0200
@@ -207,7 +207,6 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL \
   Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
   Library/Efficient_Nat.thy Library/Executable_Set.thy \
-  Library/Executable_Rat.thy Library/Executable_Real.thy \
   Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
   Library/FuncSet.thy Library/Library.thy \
   Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
@@ -516,7 +515,8 @@
   Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy \
   Lambda/Lambda.thy \
   Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
-  Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
+  Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \
+  Lambda/StrongNorm.thy Lambda/Type.thy \
   Lambda/WeakNorm.thy Lambda/ROOT.ML \
   Lambda/document/root.bib Lambda/document/root.tex
 	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda