Fix unescaped expressions breaking latex output in Record.thy
Expressions containing _ and ^ need to be adjusted or antiquoted in
text comments for latex compatibility. This is in fact a little
annoying, since it makes the comment less readable in both source
and HTML form.
lcp paulson
norbert.schirmer@web.de schirmer
urbanc@in.tum.de urbanc
nipkow@lapbroy100.local nipkow
chaieb@chaieb-laptop chaieb
immler@in.tum.de immler