# HG changeset patch
# User urbanc
# Date 1213257825 -7200
# Node ID 587ad1fba128c3f26edeb20f3c04cfd31b8f797e
# Parent  8d747de5c73ee60e26d33acd07c1c4920f6516fc
added CK_Machine to the nominal section

diff -r 8d747de5c73e -r 587ad1fba128 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jun 12 09:56:28 2008 +0200
+++ b/src/HOL/IsaMakefile	Thu Jun 12 10:03:45 2008 +0200
@@ -811,6 +811,7 @@
 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
 
 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
+  Nominal/Examples/CK_Machine.thy \
   Nominal/Examples/CR.thy \
   Nominal/Examples/CR_Takahashi.thy \
   Nominal/Examples/Class.thy \