theory Test imports Main begin term \x\<^latex>\%ignored @{text} \\ end