src/HOL/Metis_Examples/Type_Encodings.thy
changeset 48146 14e317033809
parent 48098 dd611ab202a8
child 48664 81755fd809be
equal deleted inserted replaced
48145:f7b31782e632 48146:14e317033809
    25 val type_encs =
    25 val type_encs =
    26   ["erased",
    26   ["erased",
    27    "poly_guards",
    27    "poly_guards",
    28    "poly_guards?",
    28    "poly_guards?",
    29    "poly_guards??",
    29    "poly_guards??",
    30    "poly_guards@?",
    30    "poly_guards@",
    31    "poly_tags",
    31    "poly_tags",
    32    "poly_tags?",
    32    "poly_tags?",
    33    "poly_tags??",
    33    "poly_tags??",
       
    34    "poly_tags@",
    34    "poly_args",
    35    "poly_args",
    35    "poly_args?",
    36    "poly_args?",
    36    "raw_mono_guards",
    37    "raw_mono_guards",
    37    "raw_mono_guards?",
    38    "raw_mono_guards?",
    38    "raw_mono_guards??",
    39    "raw_mono_guards??",
    39    "raw_mono_guards@?",
    40    "raw_mono_guards@",
    40    "raw_mono_tags",
    41    "raw_mono_tags",
    41    "raw_mono_tags?",
    42    "raw_mono_tags?",
    42    "raw_mono_tags??",
    43    "raw_mono_tags??",
       
    44    "raw_mono_tags@",
    43    "raw_mono_args",
    45    "raw_mono_args",
    44    "raw_mono_args?",
    46    "raw_mono_args?",
    45    "mono_guards",
    47    "mono_guards",
    46    "mono_guards?",
    48    "mono_guards?",
    47    "mono_guards??",
    49    "mono_guards??",