Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
changeset 2895 65efa1c7563c
parent 2869 9c0df9901acf
child 2998 f0fab367453a
equal deleted inserted replaced
2894:8ec94871de1e 2895:65efa1c7563c
     1 header {* CPS transformation of Danvy and Nielsen *}
     1 header {* CPS transformation of Danvy and Nielsen *}
     2 theory DanvyNielsen
     2 theory CPS2_DanvyNielsen
     3 imports Lt
     3 imports Lt
     4 begin
     4 begin
     5 
     5 
     6 nominal_datatype cpsctxt =
     6 nominal_datatype cpsctxt =
     7   Hole
     7   Hole