src/Pure/type.ML
changeset 34272 95df5e6dd41c
parent 33941 40408e6b833b
child 35359 3ec03a3cd9d0
equal deleted inserted replaced
34271:70af06abb13d 34272:95df5e6dd41c
    17    {classes: Name_Space.T * Sorts.algebra,
    17    {classes: Name_Space.T * Sorts.algebra,
    18     default: sort,
    18     default: sort,
    19     types: decl Name_Space.table,
    19     types: decl Name_Space.table,
    20     log_types: string list}
    20     log_types: string list}
    21   val empty_tsig: tsig
    21   val empty_tsig: tsig
    22   val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig
       
    23   val defaultS: tsig -> sort
    22   val defaultS: tsig -> sort
    24   val logical_types: tsig -> string list
    23   val logical_types: tsig -> string list
    25   val eq_sort: tsig -> sort * sort -> bool
    24   val eq_sort: tsig -> sort * sort -> bool
    26   val subsort: tsig -> sort * sort -> bool
    25   val subsort: tsig -> sort * sort -> bool
    27   val of_sort: tsig -> typ * sort -> bool
    26   val of_sort: tsig -> typ * sort -> bool