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/BNF_Cardinal_Order_Relation.thy
changeset 82248 e8c96013ea8a
parent 81125 ec121999a9cb 
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -1104,7 +1104,16 @@
 
 lemma natLeq_Preorder: "Preorder natLeq"
   unfolding preorder_on_def
-  by (auto simp add: natLeq_Refl natLeq_trans)
+proof (intro conjI)
+  show "natLeq \<subseteq> Field natLeq \<times> Field natLeq"
+    unfolding natLeq_def Field_def by blast
+next
+  show "Refl natLeq"
+    using natLeq_Refl .
+next
+  show "trans natLeq"
+    using natLeq_trans .
+qed
 
 lemma natLeq_antisym: "antisym natLeq"
   unfolding antisym_def natLeq_def by auto
isabelle