Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper Thm.transfer (required for zproofs);
authorwenzelm
Sun, 17 Dec 2023 22:57:20 +0100
changeset 79274 fb8ed7fbb537
parent 79273 d1e5f6d1ddca
child 79275 8368160d3c65
proper Thm.transfer (required for zproofs);
src/HOL/Tools/Transfer/transfer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Transfer/transfer.ML	Sun Dec 17 21:43:14 2023 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Sun Dec 17 22:57:20 2023 +0100
@@ -385,7 +385,7 @@
 (** Adding transfer domain rules **)
 
 fun prep_transfer_domain_thm ctxt =
-  abstract_equalities_domain ctxt o detect_transfer_rules
+  abstract_equalities_domain ctxt o detect_transfer_rules o Thm.transfer' ctxt
 
 fun add_transfer_domain_thm thm ctxt =
   (add_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
isabelle