diff -r 4ec8e654112f -r 2865a6618cba src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/Tools/Code_Generator.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -39,8 +39,8 @@
 code_datatype holds
 
 lemma implies_code [code]:
+  "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
   "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
-  "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
 proof -
   show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
   proof