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/Transitive_Closure.thy
changeset 82774 2865a6618cba
parent 82695 d93ead9ac6df 
--- a/src/HOL/Transitive_Closure.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -951,13 +951,13 @@
   where relpowp_code_def [code_abbrev]: "relpowp = compow"
 
 lemma [code]:
-  "relpow (Suc n) R = (relpow n R) O R"
   "relpow 0 R = Id"
+  "relpow (Suc n) R = relpow n R O R"
   by (simp_all add: relpow_code_def)
 
 lemma [code]:
-  "relpowp (Suc n) R = (R ^^ n) OO R"
   "relpowp 0 R = HOL.eq"
+  "relpowp (Suc n) R = relpowp n R OO R"
   by (simp_all add: relpowp_code_def)
 
 hide_const (open) relpow
isabelle