81 * Comment.text -> bool -> theory -> ProofHistory.T |
81 * Comment.text -> bool -> theory -> ProofHistory.T |
82 val lemma: (bstring * Args.src list * (string * (string list * string list))) |
82 val lemma: (bstring * Args.src list * (string * (string list * string list))) |
83 * Comment.text -> bool -> theory -> ProofHistory.T |
83 * Comment.text -> bool -> theory -> ProofHistory.T |
84 val lemma_i: (bstring * theory attribute list * (term * (term list * term list))) |
84 val lemma_i: (bstring * theory attribute list * (term * (term list * term list))) |
85 * Comment.text -> bool -> theory -> ProofHistory.T |
85 * Comment.text -> bool -> theory -> ProofHistory.T |
86 val assume: (string * Args.src list * (string * (string list * string list)) list) |
86 val assume: ((string * Args.src list * (string * (string list * string list)) list) |
87 * Comment.text -> ProofHistory.T -> ProofHistory.T |
87 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
88 val assume_i: (string * Proof.context attribute list * (term * (term list * term list)) list) |
88 val assume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list) |
89 * Comment.text -> ProofHistory.T -> ProofHistory.T |
89 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
90 val presume: (string * Args.src list * (string * (string list * string list)) list) |
90 val presume: ((string * Args.src list * (string * (string list * string list)) list) |
91 * Comment.text -> ProofHistory.T -> ProofHistory.T |
91 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
92 val presume_i: (string * Proof.context attribute list * (term * (term list * term list)) list) |
92 val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list) |
93 * Comment.text -> ProofHistory.T -> ProofHistory.T |
93 * Comment.text) list -> ProofHistory.T -> ProofHistory.T |
94 val local_def: (string * Args.src list * ((string * string option) * (string * string list))) |
94 val local_def: (string * Args.src list * ((string * string option) * (string * string list))) |
95 * Comment.text -> ProofHistory.T -> ProofHistory.T |
95 * Comment.text -> ProofHistory.T -> ProofHistory.T |
96 val local_def_i: (string * Args.src list * ((string * typ) * (term * term list))) |
96 val local_def_i: (string * Args.src list * ((string * typ) * (term * term list))) |
97 * Comment.text -> ProofHistory.T -> ProofHistory.T |
97 * Comment.text -> ProofHistory.T -> ProofHistory.T |
98 val show: (string * Args.src list * (string * (string list * string list))) |
98 val show: (string * Args.src list * (string * (string list * string list))) |
271 val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore; |
271 val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore; |
272 |
272 |
273 |
273 |
274 (* statements *) |
274 (* statements *) |
275 |
275 |
|
276 local |
|
277 |
276 fun global_statement f (name, src, s) int thy = |
278 fun global_statement f (name, src, s) int thy = |
277 ProofHistory.init (Toplevel.undo_limit int) |
279 ProofHistory.init (Toplevel.undo_limit int) |
278 (f name (map (Attrib.global_attribute thy) src) s thy); |
280 (f name (map (Attrib.global_attribute thy) src) s thy); |
279 |
281 |
280 fun global_statement_i f (name, atts, t) int thy = |
282 fun global_statement_i f (name, atts, t) int thy = |
282 |
284 |
283 fun local_statement f g (name, src, s) = ProofHistory.apply (fn state => |
285 fun local_statement f g (name, src, s) = ProofHistory.apply (fn state => |
284 f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state)); |
286 f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state)); |
285 |
287 |
286 fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g); |
288 fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g); |
|
289 |
|
290 fun multi_statement f args = ProofHistory.apply (fn state => |
|
291 f (map (fn (name, src, s) => |
|
292 (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state); |
|
293 |
|
294 fun multi_statement_i f args = ProofHistory.apply (f args); |
|
295 |
|
296 in |
287 |
297 |
288 val theorem = global_statement Proof.theorem o Comment.ignore; |
298 val theorem = global_statement Proof.theorem o Comment.ignore; |
289 val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore; |
299 val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore; |
290 val lemma = global_statement Proof.lemma o Comment.ignore; |
300 val lemma = global_statement Proof.lemma o Comment.ignore; |
291 val lemma_i = global_statement_i Proof.lemma_i o Comment.ignore; |
301 val lemma_i = global_statement_i Proof.lemma_i o Comment.ignore; |
292 val assume = local_statement Proof.assume I o Comment.ignore; |
302 val assume = multi_statement Proof.assume o map Comment.ignore; |
293 val assume_i = local_statement_i Proof.assume_i I o Comment.ignore; |
303 val assume_i = multi_statement_i Proof.assume_i o map Comment.ignore; |
294 val presume = local_statement Proof.presume I o Comment.ignore; |
304 val presume = multi_statement Proof.presume o map Comment.ignore; |
295 val presume_i = local_statement_i Proof.presume_i I o Comment.ignore; |
305 val presume_i = multi_statement_i Proof.presume_i o map Comment.ignore; |
296 val local_def = local_statement LocalDefs.def I o Comment.ignore; |
306 val local_def = local_statement LocalDefs.def I o Comment.ignore; |
297 val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore; |
307 val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore; |
298 val show = local_statement (Proof.show Seq.single) I o Comment.ignore; |
308 val show = local_statement (Proof.show Seq.single) I o Comment.ignore; |
299 val show_i = local_statement_i (Proof.show_i Seq.single) I o Comment.ignore; |
309 val show_i = local_statement_i (Proof.show_i Seq.single) I o Comment.ignore; |
300 val have = local_statement (Proof.have Seq.single) I o Comment.ignore; |
310 val have = local_statement (Proof.have Seq.single) I o Comment.ignore; |
302 val thus = local_statement (Proof.show Seq.single) Proof.chain o Comment.ignore; |
312 val thus = local_statement (Proof.show Seq.single) Proof.chain o Comment.ignore; |
303 val thus_i = local_statement_i (Proof.show_i Seq.single) Proof.chain o Comment.ignore; |
313 val thus_i = local_statement_i (Proof.show_i Seq.single) Proof.chain o Comment.ignore; |
304 val hence = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore; |
314 val hence = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore; |
305 val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore; |
315 val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore; |
306 |
316 |
|
317 end; |
|
318 |
307 |
319 |
308 (* blocks *) |
320 (* blocks *) |
309 |
321 |
310 val begin_block = ProofHistory.apply Proof.begin_block; |
322 val begin_block = ProofHistory.apply Proof.begin_block; |
311 val next_block = ProofHistory.apply Proof.next_block; |
323 val next_block = ProofHistory.apply Proof.next_block; |