Session Universal_Turing_Machine
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Binary_Nat
HOL-Library.Code_Target_Nat
HOL-Library.Code_Target_Numeral
Turing
Turing_aux
BlanksDoNotMatter
ComposableTMs
ComposedTMs
Numerals
Numerals_Ex
Turing_Hoare
SemiIdTM
Turing_HaltingConditions
OneStrokeTM
WeakCopyTM
StrongCopyTM
TuringDecidable
TuringReducible
HOL-Library.Nat_Bijection
SimpleGoedelEncoding
HaltingProblems_K_H
HaltingProblems_K_aux
TuringComputable
DitherTM
CopyTM
TuringUnComputable_H2
TuringUnComputable_H2_original
Abacus_Mopup
Abacus
Abacus_alt_Compile
Abacus_Hoare
Rec_Def
Rec_Ex
Recursive
HOL-Library.Discrete
Recs_alt_Def
Recs_alt_Ex
UF
UTM
GeneratedCode