equal
deleted
inserted
replaced
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 |
13 |
14 no_document |
14 no_document |
15 use_thys ["turing_basic", |
15 use_thys ["thys/turing_basic"(*, |
16 "uncomputable", |
16 "thys/truing_hoare", |
17 "abacus", |
17 "thys/uncomputable", |
18 "rec_def", |
18 "thys/abacus", |
19 "recursive", |
19 "thys/rec_def", |
20 "UF", |
20 "thys/recursive"*)] |
21 "UTM"] |
|