changed to not compile Iteration and Recursion, but Lam_Funs instead
authorurbanc
Wed, 01 Nov 2006 19:03:30 +0100
changeset 21142 a56a839e9feb
parent 21141 f0b5e6254a1f
child 21143 56695d1f45cf
changed to not compile Iteration and Recursion, but Lam_Funs instead
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