Nominal/ExCoreHaskell.thy
changeset 1653 a2142526bb01
parent 1651 f731e9aff866
child 1656 c9d3dda79fe3
equal deleted inserted replaced
1652:3b9c05d158f3 1653:a2142526bb01
     4 
     4 
     5 (* core haskell *)
     5 (* core haskell *)
     6 
     6 
     7 ML {* val _ = recursive := false *}
     7 ML {* val _ = recursive := false *}
     8 ML {* val _ = cheat_const_rsp := true *}
     8 ML {* val _ = cheat_const_rsp := true *}
     9 ML {* val _ = cheat_alpha_bn_rsp := true *}
       
    10 atom_decl var
     9 atom_decl var
    11 atom_decl tvar
    10 atom_decl tvar
    12 
    11 
    13 (* there are types, coercion types and regular types list-data-structure *)
    12 (* there are types, coercion types and regular types list-data-structure *)
    14 
    13