Hi,There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by "hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes an error in a proof.
The proof passes even through there's an error 'Undefined fact: "add_assoc"'. I attach a screen shot showing the error.
Trying to fix that problem, I ran Sledgehammer and have a more serious problem, which is that Cygwin temp files can't be deleted, which causes the prover process to terminate. I'll put that that in another email.
Description: PNG image