equal
deleted
inserted
replaced
70 |
70 |
71 use "Concurrent/synchronized.ML"; |
71 use "Concurrent/synchronized.ML"; |
72 if Multithreading.available then () |
72 if Multithreading.available then () |
73 else use "Concurrent/synchronized_sequential.ML"; |
73 else use "Concurrent/synchronized_sequential.ML"; |
74 |
74 |
|
75 use "Concurrent/time_limit.ML"; |
|
76 if Multithreading.available then () |
|
77 else use "Concurrent/time_limit_dummy.ML"; |
|
78 |
75 if Multithreading.available |
79 if Multithreading.available |
76 then use "Concurrent/bash.ML" |
80 then use "Concurrent/bash.ML" |
77 else use "Concurrent/bash_sequential.ML"; |
81 else use "Concurrent/bash_sequential.ML"; |
78 |
82 |
79 fun bash s = |
83 fun bash s = |