src/HOL/Predicate.thy

--- a/src/HOL/Predicate.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Predicate.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -533,16 +533,16 @@
 instance by standard simp
 
 end
-    
-lemma [code]:
-  "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" for P Q :: "'a pred"
-  by auto
 
 lemma [code nbe]:
   "HOL.equal P P \<longleftrightarrow> True" for P :: "'a pred"
   by (fact equal_refl)
 
 lemma [code]:
+  "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" for P Q :: "'a pred"
+  by auto
+
+lemma [code]:
   "case_pred f P = f (eval P)"
   by (fact pred.case_eq_if)