# HG changeset patch
# User urbanc
# Date 1174061856 -3600
# Node ID f982e73e36dec9224dbdbef3ad27731eae0cc5c1
# Parent  013dbd8234f0a6a1676990016f554f896841a115
adjusted for the example file SOS.thy

diff -r 013dbd8234f0 -r f982e73e36de src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 16 17:12:52 2007 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 16 17:17:36 2007 +0100
@@ -752,7 +752,8 @@
   Nominal/Examples/Lam_Funs.thy	\
   Nominal/Examples/SN.thy \
   Nominal/Examples/Weakening.thy \
-  Nominal/Examples/Crary.thy
+  Nominal/Examples/Crary.thy \
+  Nominal/Examples/SOS.thy
 	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
 
 
diff -r 013dbd8234f0 -r f982e73e36de src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Mar 16 17:12:52 2007 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Mar 16 17:17:36 2007 +0100
@@ -13,4 +13,5 @@
 use_thy "Lambda_mu";
 use_thy "SN";
 use_thy "Weakening";
-use_thy "Crary";
\ No newline at end of file
+use_thy "Crary";
+use_thy "SOS";
\ No newline at end of file