equal
deleted
inserted
replaced
10 |
10 |
11 val ml = "isabelle" |
11 val ml = "isabelle" |
12 |
12 |
13 fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y) |
13 fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y) |
14 |
14 |
15 fun critical e () = NAMED_CRITICAL "metis" e |
15 local |
|
16 val lock = Mutex.mutex (); |
|
17 in |
|
18 fun critical e () = Multithreading.synchronized "metis" lock e |
|
19 end; |
16 |
20 |
17 val randomWord = Random.nextWord |
21 val randomWord = Random.nextWord |
18 val randomBool = Random.nextBool |
22 val randomBool = Random.nextBool |
19 val randomInt = Random.nextInt |
23 val randomInt = Random.nextInt |
20 val randomReal = Random.nextReal |
24 val randomReal = Random.nextReal |