--- a/src/HOL/Transfer.thy Thu Aug 08 12:11:40 2019 +0200
+++ b/src/HOL/Transfer.thy Thu Aug 08 12:18:27 2019 +0200
@@ -229,6 +229,22 @@
end
+lemma is_equality_lemma: "(\<And>R. is_equality R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (=))"
+ apply (unfold is_equality_def)
+ apply (rule equal_intr_rule)
+ apply (drule meta_spec)
+ apply (erule meta_mp)
+ apply (rule refl)
+ apply simp
+ done
+
+lemma Domainp_lemma: "(\<And>R. Domainp T = R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (Domainp T))"
+ apply (rule equal_intr_rule)
+ apply (drule meta_spec)
+ apply (erule meta_mp)
+ apply (rule refl)
+ apply simp
+ done
ML_file \<open>Tools/Transfer/transfer.ML\<close>
declare refl [transfer_rule]