src/Tools/Code_Generator.thy

   by (unfold holds_def) (rule reflexive)
 
 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
     assume "PROP holds \<Longrightarrow> PROP P"
     then show "PROP P" using holds .