author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Fri, 18 Jan 2013 11:40:01 +0000 | |
changeset 48 | 559e5c6e5113 |
parent 2 | ROOT1.ML@26b17f2d583e |
child 55 | cd4ef33c8fb1 |
permissions | -rw-r--r-- |
2
26b17f2d583e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
no_document |
48
559e5c6e5113
updated to ITP and updated directories
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
2
diff
changeset
|
2 |
use_thys ["../thys/turing_basic", |
559e5c6e5113
updated to ITP and updated directories
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
2
diff
changeset
|
3 |
"../thys/uncomputable"(*, |
559e5c6e5113
updated to ITP and updated directories
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
2
diff
changeset
|
4 |
"../thys/abacus"*)]; |
2
26b17f2d583e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
26b17f2d583e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
use_thys ["Paper"] |