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/Tools/Code_Generator.thy
changeset 82774 2865a6618cba
parent 70009 435fb018e8ee 
--- 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
isabelle