adjusted for the example file SOS.thy
authorurbanc
Fri Mar 16 17:17:36 2007 +0100 (2007-03-16)
changeset 22448f982e73e36de
parent 22447 013dbd8234f0
child 22449 ece6952a8975
adjusted for the example file SOS.thy
src/HOL/IsaMakefile
src/HOL/Nominal/Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Mar 16 17:12:52 2007 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Mar 16 17:17:36 2007 +0100
     1.3 @@ -752,7 +752,8 @@
     1.4    Nominal/Examples/Lam_Funs.thy	\
     1.5    Nominal/Examples/SN.thy \
     1.6    Nominal/Examples/Weakening.thy \
     1.7 -  Nominal/Examples/Crary.thy
     1.8 +  Nominal/Examples/Crary.thy \
     1.9 +  Nominal/Examples/SOS.thy
    1.10  	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
    1.11  
    1.12  
     2.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Mar 16 17:12:52 2007 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Mar 16 17:17:36 2007 +0100
     2.3 @@ -13,4 +13,5 @@
     2.4  use_thy "Lambda_mu";
     2.5  use_thy "SN";
     2.6  use_thy "Weakening";
     2.7 -use_thy "Crary";
     2.8 \ No newline at end of file
     2.9 +use_thy "Crary";
    2.10 +use_thy "SOS";
    2.11 \ No newline at end of file