equal
deleted
inserted
replaced
81 Theorem of theory attribute list | (*top-level theorem*) |
81 Theorem of theory attribute list | (*top-level theorem*) |
82 Lemma of theory attribute list | (*top-level lemma*) |
82 Lemma of theory attribute list | (*top-level lemma*) |
83 Goal of context attribute list | (*intermediate result, solving subgoal*) |
83 Goal of context attribute list | (*intermediate result, solving subgoal*) |
84 Aux of context attribute list ; (*intermediate result*) |
84 Aux of context attribute list ; (*intermediate result*) |
85 |
85 |
86 val theoremN = "theorem"; |
|
87 val kind_name = |
86 val kind_name = |
88 fn Theorem _ => theoremN | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have"; |
87 fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have"; |
89 |
88 |
90 type goal = |
89 type goal = |
91 (kind * (*result kind*) |
90 (kind * (*result kind*) |
92 string * (*result name*) |
91 string * (*result name*) |
93 cterm list * (*result assumptions*) |
92 cterm list * (*result assumptions*) |
629 Theorem atts => if_none alt_atts atts |
628 Theorem atts => if_none alt_atts atts |
630 | Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma] |
629 | Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma] |
631 | _ => raise STATE ("No global goal!", state)); |
630 | _ => raise STATE ("No global goal!", state)); |
632 |
631 |
633 val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state); |
632 val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state); |
634 in (thy', (theoremN, name, result')) end; |
633 in (thy', (kind_name kind, name, result')) end; |
635 |
634 |
636 fun qed meth_fun alt_name alt_atts state = |
635 fun qed meth_fun alt_name alt_atts state = |
637 state |
636 state |
638 |> finish_proof true meth_fun |
637 |> finish_proof true meth_fun |
639 |> Seq.hd |
638 |> Seq.hd |