equal
deleted
inserted
replaced
71 val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context |
71 val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context |
72 val import: bool -> thm list -> Proof.context -> |
72 val import: bool -> thm list -> Proof.context -> |
73 (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context |
73 (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context |
74 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
74 val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
75 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
75 val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list |
|
76 val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context |
76 val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context |
77 val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context |
77 val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context |
78 val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context |
78 val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context |
79 val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context |
79 val warn_extra_tfrees: Proof.context -> Proof.context -> unit |
80 val warn_extra_tfrees: Proof.context -> Proof.context -> unit |
80 val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list |
81 val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list |