| changeset 3245 | 017e33849f4d |
| parent 3235 | 5ebd327ffb96 |
| 3244:a44479bde681 | 3245:017e33849f4d |
|---|---|
1 header {* CPS transformation of Danvy and Filinski *} |
1 (* CPS transformation of Danvy and Filinski *) |
2 theory CPS3_DanvyFilinski imports Lt begin |
2 theory CPS3_DanvyFilinski imports Lt begin |
3 |
3 |
4 nominal_function |
4 nominal_function |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
6 and |
6 and |