Fix aatgroup for the experimental kernel

HOL-Theorem-Prover · Aug 27, 2024 · de7fb61 · de7fb61
1 parent 2cb041d
commit de7fb61
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/examples/algebra/aat/aatgroupScript.sml b/examples/algebra/aat/aatgroupScript.sml
@@ -481,6 +481,7 @@ Theorem monoid_iso_isgroup:
 Proof
   xfer_back_tac[] >>
   rw[monoidTheory.MonoidIso_def, monoidTheory.MonoidHomo_def] >>
+  rename [‘BIJ f g.carrier h.carrier’] >>
   ‘GroupHomo f g h’ by simp[groupTheory.GroupHomo_def] >>
   ‘GroupIso f g h’ by simp[groupTheory.GroupIso_def] >>
   metis_tac[groupTheory.group_iso_group]