Something is wrong with the markup in theory Quotient.thy: *** [819]) (./Quotient.tex [820] [821] [822] [823] [824] *** ! Missing $ inserted. *** <inserted text> *** $ *** l.797 ...vable; which is why we need to use apply_ *** rsp and *** ! Missing $ inserted. d1c15bf767c0 tip Larry