77 val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T |
77 val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T |
78 val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
78 val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
79 val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
79 val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
80 val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
80 val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
81 val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
81 val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
82 val invoke_case: string * Comment.text -> ProofHistory.T -> ProofHistory.T |
82 val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T |
|
83 val invoke_case_i: (string * Proof.context attribute list) * Comment.text |
|
84 -> ProofHistory.T -> ProofHistory.T |
83 val theorem: (bstring * Args.src list * (string * (string list * string list))) |
85 val theorem: (bstring * Args.src list * (string * (string list * string list))) |
84 * Comment.text -> bool -> theory -> ProofHistory.T |
86 * Comment.text -> bool -> theory -> ProofHistory.T |
85 val theorem_i: (bstring * theory attribute list * (term * (term list * term list))) |
87 val theorem_i: (bstring * theory attribute list * (term * (term list * term list))) |
86 * Comment.text -> bool -> theory -> ProofHistory.T |
88 * Comment.text -> bool -> theory -> ProofHistory.T |
87 val lemma: (bstring * Args.src list * (string * (string list * string list))) |
89 val lemma: (bstring * Args.src list * (string * (string list * string list))) |
286 |
288 |
287 val fix = ProofHistory.apply o Proof.fix o map Comment.ignore; |
289 val fix = ProofHistory.apply o Proof.fix o map Comment.ignore; |
288 val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore; |
290 val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore; |
289 val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore; |
291 val match_bind = ProofHistory.apply o Proof.match_bind o map Comment.ignore; |
290 val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore; |
292 val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore; |
291 val invoke_case = ProofHistory.apply o Proof.invoke_case o Comment.ignore; |
293 |
|
294 fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state => |
|
295 Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state); |
|
296 val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore; |
292 |
297 |
293 |
298 |
294 (* statements *) |
299 (* statements *) |
295 |
300 |
296 local |
301 local |