only testing theory LSC_Examples when GHC is installed on the machine
authorbulwahn
Fri, 11 Mar 2011 10:37:45 +0100
changeset 41914 4ef7e6e317fa
parent 41913 34360908cb78
child 41915 fba21941bdc5
only testing theory LSC_Examples when GHC is installed on the machine
src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 11 10:37:43 2011 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 11 10:37:45 2011 +0100
@@ -73,10 +73,12 @@
   "Quicksort",
   "Birthday_Paradoxon",
   "List_to_Set_Comprehension_Examples",
-  "Set_Algebras",
-  "LSC_Examples"
+  "Set_Algebras"
 ];
 
+if getenv "EXEC_GHC" = "" then ()
+else use_thy "LSC_Examples";
+
 use_thy "SVC_Oracle";
 if getenv "SVC_HOME" = "" then ()
 else use_thy "svc_test";