From de7fb61814acbb0f1393821a7e89b4ce589a41fb Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 28 Aug 2024 09:57:16 +1000 Subject: [PATCH] Fix aatgroup for the experimental kernel --- examples/algebra/aat/aatgroupScript.sml | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/algebra/aat/aatgroupScript.sml b/examples/algebra/aat/aatgroupScript.sml index 134a65310f..8a1392b6d5 100644 --- 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]