Auto-insert error in current development version
Lawrence Paulson
lp15 at cam.ac.uk
Thu Mar 5 19:49:14 CET 2026
In recent versions e.g. 592248e8358d+ the “self-insert” feature of sledgehammer, induction proofs, etc., has stopped working.
Larry
More information about the isabelle-dev
mailing list