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

Update to latest development version of Isabelle.
Some checks are pending
ci/woodpecker/push/build Pipeline is pending
Details

Browse Source
This commit is contained in:
Achim D. Brucker 2025-03-13 14:45:00 +00:00
parent 1aeb275ea6
commit 95b30e8b5f
2 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Isabelle_DOF-Proofs/Reification_Test.thy
View File

@ -403,7 +403,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
term*\<open>@{thm \<open>Reification_Test.identity_conc\<close>}\<close>
@ -434,7 +434,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
declare[[show_sorts = false]]
@ -458,7 +458,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
prf test
@ -485,7 +485,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
prf test2
@ -510,7 +510,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
prf test3
@ -535,7 +535,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
prf test4
@ -560,7 +560,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
prf symmetric
@ -635,7 +635,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
ML\<open>
val thy = \<^theory>;
@ -700,7 +700,7 @@ ML\<open>
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
(fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
ML\<open>

4
Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
View File

@ -162,12 +162,12 @@ fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos =
val thm_name = HOLogic.dest_string term
val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name
val body = Proofterm.strip_thm_body (Thm.proof_body_of thm)
val all_thms_name = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] []
val all_thms_name = Proofterm.fold_body_thms (fn {thm_name, ...} => insert (op =) thm_name) [body] []
(*val all_thms = map (Proof_Context.get_thm (Proof_Context.init_global thy)) all_thms_name*)
(*val all_proofs = map (Proof_Syntax.standard_proof_of
{full = true, expand_name = Thm.expand_name thm}) all_thms*)
(*in HOLogic.mk_list \<^Type>\<open>thm\<close> (map (fn proof => \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof) all_proofs) end*)
in HOLogic.mk_list \<^typ>\<open>string\<close> (map HOLogic.mk_string all_thms_name) end
in HOLogic.mk_list \<^typ>\<open>string\<close> (map HOLogic.mk_string (map (Proof_Context.print_thm_name (Proof_Context.init_global thy)) all_thms_name)) end
fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos =
case term_option of