133 -> ProofHistory.T -> ProofHistory.T |
133 -> ProofHistory.T -> ProofHistory.T |
134 val qed: (Method.text * Comment.interest) option * Comment.text |
134 val qed: (Method.text * Comment.interest) option * Comment.text |
135 -> Toplevel.transition -> Toplevel.transition |
135 -> Toplevel.transition -> Toplevel.transition |
136 val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option) |
136 val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option) |
137 * Comment.text -> Toplevel.transition -> Toplevel.transition |
137 * Comment.text -> Toplevel.transition -> Toplevel.transition |
|
138 val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
138 val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
139 val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
139 val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
140 val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
140 val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
141 val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
141 val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
142 val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition |
142 val get_thmss: (string * Args.src list) list -> Proof.state -> thm list |
143 val get_thmss: (string * Args.src list) list -> Proof.state -> thm list |
143 val also: ((string * Args.src list) list * Comment.interest) option * Comment.text |
144 val also: ((string * Args.src list) list * Comment.interest) option * Comment.text |
144 -> Toplevel.transition -> Toplevel.transition |
145 -> Toplevel.transition -> Toplevel.transition |
436 |
437 |
437 |
438 |
438 (* local endings *) |
439 (* local endings *) |
439 |
440 |
440 val local_qed = |
441 val local_qed = |
441 proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest; |
442 proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest; |
442 |
443 |
443 fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y); |
444 fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y); |
444 |
445 |
445 val local_terminal_proof = |
446 val local_terminal_proof = |
446 proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests; |
447 proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests; |
447 |
448 |
|
449 val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof); |
448 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof); |
450 val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof); |
449 val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof); |
|
450 val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof); |
451 val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof); |
|
452 val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof); |
451 |
453 |
452 |
454 |
453 (* global endings *) |
455 (* global endings *) |
454 |
456 |
455 fun global_result finish = Toplevel.proof_to_theory (fn prf => |
457 fun global_result finish = Toplevel.proof_to_theory (fn prf => |
457 val state = ProofHistory.current prf; |
459 val state = ProofHistory.current prf; |
458 val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF; |
460 val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF; |
459 val (thy, res as {kind, name, thm}) = finish state; |
461 val (thy, res as {kind, name, thm}) = finish state; |
460 in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end); |
462 in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end); |
461 |
463 |
462 val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest; |
464 val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest; |
463 val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests; |
465 val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests; |
|
466 val global_default_proof = global_result Method.global_default_proof; |
464 val global_immediate_proof = global_result Method.global_immediate_proof; |
467 val global_immediate_proof = global_result Method.global_immediate_proof; |
465 val global_default_proof = global_result Method.global_default_proof; |
|
466 val global_skip_proof = global_result SkipProof.global_skip_proof; |
468 val global_skip_proof = global_result SkipProof.global_skip_proof; |
|
469 val global_done_proof = global_result Method.global_done_proof; |
467 |
470 |
468 |
471 |
469 (* common endings *) |
472 (* common endings *) |
470 |
473 |
471 fun qed (meth, comment) = local_qed meth o global_qed meth; |
474 fun qed (meth, comment) = local_qed meth o global_qed meth; |
472 fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths; |
475 fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths; |
|
476 fun default_proof comment = local_default_proof o global_default_proof; |
473 fun immediate_proof comment = local_immediate_proof o global_immediate_proof; |
477 fun immediate_proof comment = local_immediate_proof o global_immediate_proof; |
474 fun default_proof comment = local_default_proof o global_default_proof; |
478 fun done_proof comment = local_done_proof o global_done_proof; |
475 fun skip_proof comment = local_skip_proof o global_skip_proof; |
479 fun skip_proof comment = local_skip_proof o global_skip_proof; |
476 |
480 |
477 fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current); |
481 fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current); |
478 |
482 |
479 |
483 |