src/HOL/Metis_Examples/Type_Encodings.thy
changeset 47048 3347c853d8e2
parent 46733 4a03b30e04cb
child 48091 64025f5405a4
equal deleted inserted replaced
47047:10bece4ac87e 47048:3347c853d8e2
    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_guards!",
    31    "poly_guards!",
    32    "poly_guards!!",
    32    "poly_guards!!",
    33    "poly_guards@!",
    33    (* "poly_guards@!", *)
    34    "poly_tags",
    34    "poly_tags",
    35    "poly_tags?",
    35    "poly_tags?",
    36    "poly_tags??",
    36    "poly_tags??",
    37    "poly_tags!",
    37    "poly_tags!",
    38    "poly_tags!!",
    38    "poly_tags!!",