Nominal/Ex/CPS/CPS1_Plotkin.thy
changeset 3245 017e33849f4d
parent 3236 e2da10806a34
equal deleted inserted replaced
3244:a44479bde681 3245:017e33849f4d
     1 header {* CPS conversion *}
     1 (* CPS conversion *)
     2 theory CPS1_Plotkin
     2 theory CPS1_Plotkin
     3 imports Lt
     3 imports Lt
     4 begin
     4 begin
     5 
     5 
     6 nominal_function
     6 nominal_function