Session Universal_Turing_Machine

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