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

Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2023-04-20 09:47:30 +02:00
parent c9de5f2293 c6dc848438
commit 2c7df482e8
1 changed files with 5 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2578,6 +2578,9 @@ ML\<open>
local
fun elaborate stmt ctxt = stmt |> map (apsnd (map (apfst (DOF_core.elaborate_term ctxt)
#> apsnd (map (DOF_core.elaborate_term ctxt)))))
fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
let
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
@ -2587,11 +2590,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
(case raw_stmt of
Element.Shows _ =>
let val stmt' = Attrib.map_specs (map prep_att) stmt
val stmt'' = stmt' |> map (fn (b, ts) =>
(b, ts |> map (fn (t', t's) =>
(DOF_core.elaborate_term ctxt t',
t's |> map (fn t'' =>
DOF_core.elaborate_term ctxt t'')))))
val stmt'' = elaborate stmt' ctxt
in (([], prems, stmt'', NONE), stmt_ctxt) end
| Element.Obtains raw_obtains =>
let
@ -2606,11 +2605,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
||> Proof_Context.restore_stmt asms_ctxt;
val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
val stmt'' = stmt' |> map (fn (b, ts) =>
(b, ts |> map (fn (t', t's) =>
(DOF_core.elaborate_term ctxt t',
t's |> map (fn t'' =>
DOF_core.elaborate_term ctxt t'')))))
val stmt'' = elaborate stmt' ctxt
in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end)
end;