Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Isabelle API update.

This commit is contained in:
Achim D. Brucker 2023-08-29 06:11:32 +01:00
parent d7f9f10ef1
commit c063287947
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2562,7 +2562,8 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt
|> prep_statement (prep_att lthy) prep_stmt elems raw_concl; |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
val atts = more_atts @ map (prep_att lthy) raw_atts; val atts = more_atts @ map (prep_att lthy) raw_atts;
val pos = Position.thread_data (); val print_cfg = {interactive = int, pos = Position.thread_data (), proof_state= false}
fun after_qed' results goal_ctxt' = fun after_qed' results goal_ctxt' =
let let
val results' = val results' =
@ -2574,12 +2575,12 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt
(map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
val lthy'' = val lthy'' =
if Binding.is_empty_atts (name, atts) then if Binding.is_empty_atts (name, atts) then
(Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy') (Proof_Display.print_results print_cfg lthy' ((kind, ""), res); lthy')
else else
let let
val ([(res_name, _)], lthy'') = val ([(res_name, _)], lthy'') =
Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res); val _ = Proof_Display.print_results print_cfg lthy' ((kind, res_name), res);
in lthy'' end; in lthy'' end;
in after_qed results' lthy'' end; in after_qed results' lthy'' end;