equal
deleted
inserted
replaced
107 val at_bottom: state -> bool |
107 val at_bottom: state -> bool |
108 val local_qed: (state -> state Seq.seq) |
108 val local_qed: (state -> state Seq.seq) |
109 -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit) |
109 -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit) |
110 -> state -> state Seq.seq |
110 -> state -> state Seq.seq |
111 val global_qed: (state -> state Seq.seq) -> state |
111 val global_qed: (state -> state Seq.seq) -> state |
112 -> (theory * (string * (string * thm list) list)) Seq.seq |
112 -> (theory * ((string * string) * (string * thm list) list)) Seq.seq |
113 val begin_block: state -> state |
113 val begin_block: state -> state |
114 val end_block: state -> state Seq.seq |
114 val end_block: state -> state Seq.seq |
115 val next_block: state -> state |
115 val next_block: state -> state |
116 end; |
116 end; |
117 |
117 |
787 theory_of state |
787 theory_of state |
788 |> locale_prefix locale (PureThy.have_thmss [Drule.kind k] |
788 |> locale_prefix locale (PureThy.have_thmss [Drule.kind k] |
789 ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))) |
789 ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))) |
790 |>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results); |
790 |>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results); |
791 val thy2 = thy1 |> PureThy.add_thmss [((cname, flat (map #2 res')), catts)] |> #1; |
791 val thy2 = thy1 |> PureThy.add_thmss [((cname, flat (map #2 res')), catts)] |> #1; |
792 in (thy2, (k, res')) end; |
792 in (thy2, ((k, cname), res')) end; |
793 |
793 |
794 (*note: clients should inspect first result only, as backtracking may destroy theory*) |
794 (*note: clients should inspect first result only, as backtracking may destroy theory*) |
795 fun global_qed finalize state = |
795 fun global_qed finalize state = |
796 state |
796 state |
797 |> end_proof true |
797 |> end_proof true |