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 ["thys/turing_basic"(*, |
15 use_thys ["thys/turing_basic", |
16 "thys/truing_hoare", |
16 "thys/turing_hoare", |
17 "thys/uncomputable", |
17 "thys/uncomputable", |
18 "thys/abacus", |
18 "thys/abacus", |
19 "thys/rec_def", |
19 "thys/rec_def", |
20 "thys/recursive"*)] |
20 "thys/recursive", |
|
21 "thys/UF"] |