Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transfer.thy
changeset 82286 4042628fffa5
parent 82284 a01ea04aa58f 
--- a/src/HOL/Transfer.thy	Sat Mar 15 22:42:29 2025 +0100
+++ b/src/HOL/Transfer.thy	Sun Mar 16 09:11:17 2025 +0100
@@ -182,11 +182,6 @@
   unfolding bi_unique_def rel_fun_def by auto
 
 lemma [simp]:
-  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
-    and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
-  by(auto simp add: left_unique_def right_unique_def)
-
-lemma [simp]:
   shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
     and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
   by(simp_all add: left_total_def right_total_def)
isabelle