# HG changeset patch
# User berghofe
# Date 1161557245 -7200
# Node ID 3cb13b06ad7258d3688596145c8303caa293c456
# Parent  1c898a0c0f2d3860435fb2d1cdb40214d8dfb1fb
Added Compile and Height examples to Nominal directory.

diff -r 1c898a0c0f2d -r 3cb13b06ad72 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 20 18:22:24 2006 +0200
+++ b/src/HOL/IsaMakefile	Mon Oct 23 00:47:25 2006 +0200
@@ -766,8 +766,9 @@
 
 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
   Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy	\
-  Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy			\
-  Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.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/Weakening.thy
 	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples