equal
deleted
inserted
replaced
1 theory UF |
1 theory UF |
2 imports Main rec_def turing_basic GCD abacus |
2 imports Rec_Def GCD Abacus |
3 begin |
3 begin |
4 |
4 |
5 text {* |
5 text {* |
6 This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined |
6 This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined |
7 in terms of recursive functions. This @{text "rec_F"} is essentially an |
7 in terms of recursive functions. This @{text "rec_F"} is essentially an |