Formalizing Splitting in Isabelle/HOL.

Ghilain Bergeron, Florent Krasnopol, Sophie Tourret

Browse the full ITP paper archive.