# HG changeset patch # User urbanc # Date 1168953085 -3600 # Node ID 2882d9cc5e75c558a9e0eac43ce432e33f15b275 # Parent 42ae57200d963830a23cd3c42b0468bda4bdbdb6 fixed typo introduced by me diff -r 42ae57200d96 -r 2882d9cc5e75 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jan 16 14:10:27 2007 +0100 +++ b/src/HOL/IsaMakefile Tue Jan 16 14:11:25 2007 +0100 @@ -734,7 +734,7 @@ HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ - Nominal/Examples/ROOT.ML + Nominal/Examples/ROOT.ML \ Nominal/Examples/CR.thy \ Nominal/Examples/Class.thy \ Nominal/Examples/Compile.thy \