adjusted for the example file SOS.thy
authorurbanc
Fri, 16 Mar 2007 17:17:36 +0100
changeset 22448 f982e73e36de
parent 22447 013dbd8234f0
child 22449 ece6952a8975
adjusted for the example file SOS.thy
src/HOL/IsaMakefile
src/HOL/Nominal/Examples/ROOT.ML
--- 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
 
 
--- 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