Nominal/Ex/CoreHaskell.thy
changeset 2398 1e6160690546
parent 2393 d9a0cf26a88c
child 2399 107c06267f33
equal deleted inserted replaced
2397:c670a849af65 2398:1e6160690546
     6 
     6 
     7 atom_decl var
     7 atom_decl var
     8 atom_decl cvar
     8 atom_decl cvar
     9 atom_decl tvar
     9 atom_decl tvar
    10 
    10 
    11 declare [[STEPS = 17]]
    11 declare [[STEPS = 18]]
    12 
    12 
    13 nominal_datatype tkind =
    13 nominal_datatype tkind =
    14   KStar
    14   KStar
    15 | KFun "tkind" "tkind"
    15 | KFun "tkind" "tkind"
    16 and ckind =
    16 and ckind =