0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
(*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
turing_basic.thy : The basic definitions of Turing Machine.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
uncomputable.thy : The existence of Turing uncomputable functions.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
the compilation of Abacus machines into Turing Machines.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
rec_def.thy: The basic definitions of Recursive Functions.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
recursive.thy : The compilation of Recursive Functions into
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
Abacus machines.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
initialization and termination processing Turing Machines.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
*)
|
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
no_document
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
use_thys ["thys/turing_basic",
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
"thys/turing_hoare",
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
"thys/uncomputable",
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
"thys/abacus",
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
"thys/rec_def",
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
"thys/recursive",
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
"thys/UF"]
|