Nominal/ExCoreHaskell.thy
changeset 1650 4b949985cf57
parent 1648 1ca332adc247
child 1651 f731e9aff866
equal deleted inserted replaced
1649:ba837d3ed37f 1650:4b949985cf57
     3 begin
     3 begin
     4 
     4 
     5 (* core haskell *)
     5 (* core haskell *)
     6 
     6 
     7 ML {* val _ = recursive := false *}
     7 ML {* val _ = recursive := false *}
     8 ML {* val _ = cheat_bn_eqvt := true *}
       
     9 ML {* val _ = cheat_bn_rsp := true *}
     8 ML {* val _ = cheat_bn_rsp := true *}
    10 ML {* val _ = cheat_const_rsp := true *}
     9 ML {* val _ = cheat_const_rsp := true *}
    11 ML {* val _ = cheat_alpha_bn_rsp := true *}
    10 ML {* val _ = cheat_alpha_bn_rsp := true *}
    12 atom_decl var
    11 atom_decl var
    13 atom_decl tvar
    12 atom_decl tvar