Isabelle/AFP sessions
Lineartime_Branchingtime_Spectrum_I