equal
deleted
inserted
replaced
60 |
60 |
61 (* ------------------------------------------------------------------------- *) |
61 (* ------------------------------------------------------------------------- *) |
62 (* Additional functions used by Nitpick (to be factored out) *) |
62 (* Additional functions used by Nitpick (to be factored out) *) |
63 (* ------------------------------------------------------------------------- *) |
63 (* ------------------------------------------------------------------------- *) |
64 |
64 |
65 val close_form : term -> term |
|
66 val get_classdef : theory -> string -> (string * term) option |
65 val get_classdef : theory -> string -> (string * term) option |
67 val norm_rhs : term -> term |
66 val norm_rhs : term -> term |
68 val get_def : theory -> string * typ -> (string * term) option |
67 val get_def : theory -> string * typ -> (string * term) option |
69 val get_typedef : theory -> typ -> (string * term) option |
68 val get_typedef : theory -> typ -> (string * term) option |
70 val is_IDT_constructor : theory -> string * typ -> bool |
69 val is_IDT_constructor : theory -> string * typ -> bool |