# HG changeset patch
# User urbanc
# Date 1162404210 -3600
# Node ID a56a839e9febab77bcdae194ee9435af560ab024
# Parent  f0b5e6254a1f88276dfce64b139dac379d147635
changed to not compile Iteration and Recursion, but Lam_Funs instead

diff -r f0b5e6254a1f -r a56a839e9feb src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Nov 01 17:57:02 2006 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 01 19:03:30 2006 +0100
@@ -767,9 +767,8 @@
 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
   Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy	\
   Nominal/Examples/Compile.thy Nominal/Examples/Fsub.thy	\
-  Nominal/Examples/Height.thy Nominal/Examples/Iteration.thy	\
-  Nominal/Examples/Lambda_mu.thy Nominal/Examples/Lam_substs.thy	\
-  Nominal/Examples/Recursion.thy Nominal/Examples/SN.thy			\
+  Nominal/Examples/Lambda_mu.thy Nominal/Examples/Lam_Funs.thy	\
+  Nominal/Examples/SN.thy			\
   Nominal/Examples/Weakening.thy
 	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples