src/HOL/ex/ROOT.ML
changeset 37280 0fb011773adc
parent 36962 5fb251d1c32f
child 37695 71e84a203c19
equal deleted inserted replaced
37251:72c7e636067b 37280:0fb011773adc
    68 ];
    68 ];
    69 
    69 
    70 HTML.with_charset "utf-8" (no_document use_thys)
    70 HTML.with_charset "utf-8" (no_document use_thys)
    71   ["Hebrew", "Chinese", "Serbian"];
    71   ["Hebrew", "Chinese", "Serbian"];
    72 
    72 
    73 (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
    73 (setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
    74   "Hilbert_Classical";
    74   "Hilbert_Classical";
    75 
    75 
    76 use_thy "SVC_Oracle";
    76 use_thy "SVC_Oracle";
    77 if getenv "SVC_HOME" = "" then ()
    77 if getenv "SVC_HOME" = "" then ()
    78 else use_thy "svc_test";
    78 else use_thy "svc_test";