src/HOL/IsaMakefile

 default: HOL
 generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
 images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
         HOL-Word TLA HOL4
 
-#Note: keep targets sorted (except for HOL-Library)
+#Note: keep targets sorted (except for HOL-Library and HOL-ex)
 test: \
   HOL-Library \
   HOL-ex \
   HOL-Auth \
   HOL-AxClasses \

   HOL-NanoJava \
   HOL-Nominal-Examples \
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-SET-Protocol \
+  HOL-SizeChange \
   HOL-Statespace \
   HOL-Subst \
       TLA-Buffer \
       TLA-Inc \
       TLA-Memory \

 
 HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
 
 $(LOG)/HOL-SizeChange.gz: $(OUT)/HOL \
 	SizeChange/Kleene_Algebras.thy SizeChange/Graphs.thy \
-	SizeChange/Misc_Tools.thy SizeChange/Criterion \
-	SizeChange/Correctness SizeChange/Interpretation \
-	SizeChange/Implementation SizeChange/Size_Change_Termination \
-	SizeChange/Examples	SizeChange/sct.ML \
+	SizeChange/Misc_Tools.thy SizeChange/Criterion.thy \
+	SizeChange/Correctness.thy SizeChange/Interpretation.thy \
+	SizeChange/Implementation.thy SizeChange/Size_Change_Termination.thy \
+	SizeChange/Examples.thy	SizeChange/sct.ML \
 	SizeChange/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL SizeChange
 
 ## HOL-Lambda