equal
deleted
inserted
replaced
21 val add_term_frees: term * term list -> term list |
21 val add_term_frees: term * term list -> term list |
22 val term_frees: term -> term list |
22 val term_frees: term -> term list |
23 val mk_defpair: term * term -> string * term |
23 val mk_defpair: term * term -> string * term |
24 val get_def: theory -> xstring -> thm |
24 val get_def: theory -> xstring -> thm |
25 val METAHYPS: (thm list -> tactic) -> int -> tactic |
25 val METAHYPS: (thm list -> tactic) -> int -> tactic |
26 val gensym: string -> string |
|
27 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) |
26 val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) |
28 val freeze_thaw: thm -> thm * (thm -> thm) |
27 val freeze_thaw: thm -> thm * (thm -> thm) |
29 end; |
28 end; |
30 |
29 |
31 structure Misc_Legacy: MISC_LEGACY = |
30 structure Misc_Legacy: MISC_LEGACY = |