equal
deleted
inserted
replaced
8 Abacus machines. |
8 Abacus machines. |
9 UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness. |
9 UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness. |
10 UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some |
10 UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some |
11 initialization and termination processing Turing Machines. |
11 initialization and termination processing Turing Machines. |
12 *) |
12 *) |
13 use_thys ["turing_basic", "uncomputable", "abacus", "rec_def", "recursive", "UF", "UTM"] |
13 |
|
14 no_document |
|
15 use_thys ["turing_basic", |
|
16 "uncomputable", |
|
17 "abacus", |
|
18 "rec_def", |
|
19 "recursive", |
|
20 "UF", |
|
21 "UTM"] |