# 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 \