equal
deleted
inserted
replaced
43 val rm_claset : unit -> unit |
43 val rm_claset : unit -> unit |
44 val rm_simpset : unit -> unit |
44 val rm_simpset : unit -> unit |
45 val rm_atpset : unit -> unit |
45 val rm_atpset : unit -> unit |
46 val rm_clasimp : unit -> unit |
46 val rm_clasimp : unit -> unit |
47 val is_fol_thms : thm list -> bool |
47 val is_fol_thms : thm list -> bool |
|
48 val tvar_classes_of_terms : term list -> string list |
|
49 val tfree_classes_of_terms : term list -> string list |
|
50 val type_consts_of_terms : theory -> term list -> string list |
48 end; |
51 end; |
49 |
52 |
50 structure ResAtp: RES_ATP = |
53 structure ResAtp: RES_ATP = |
51 struct |
54 struct |
52 |
55 |