equal
deleted
inserted
replaced
24 |
24 |
25 "Mu " :: "[idts, 'a pred] => 'a pred" ("(3[mu _./ _])" 1000) |
25 "Mu " :: "[idts, 'a pred] => 'a pred" ("(3[mu _./ _])" 1000) |
26 "Nu " :: "[idts, 'a pred] => 'a pred" ("(3[nu _./ _])" 1000) |
26 "Nu " :: "[idts, 'a pred] => 'a pred" ("(3[nu _./ _])" 1000) |
27 |
27 |
28 ML {* |
28 ML {* |
29 val trace_eindhoven = ref false; |
29 val trace_eindhoven = Unsynchronized.ref false; |
30 *} |
30 *} |
31 |
31 |
32 oracle mc_eindhoven_oracle = |
32 oracle mc_eindhoven_oracle = |
33 {* |
33 {* |
34 let |
34 let |