src/HOL/BNF/Tools/bnf_def.ML
changeset 55025 1ac0a0194428
parent 54921 862c36b6e57c
equal deleted inserted replaced
55024:05cc0dbf3a50 55025:1ac0a0194428
    26 
    26 
    27   val mapN: string
    27   val mapN: string
    28   val relN: string
    28   val relN: string
    29   val setN: string
    29   val setN: string
    30   val mk_setN: int -> string
    30   val mk_setN: int -> string
       
    31   val mk_witN: int -> string
    31 
    32 
    32   val map_of_bnf: bnf -> term
    33   val map_of_bnf: bnf -> term
    33   val sets_of_bnf: bnf -> term list
    34   val sets_of_bnf: bnf -> term list
    34   val rel_of_bnf: bnf -> term
    35   val rel_of_bnf: bnf -> term
    35 
    36