[isabelle] \<^latex>

Question: how does Isabelle estimate the size of the latex output if the string contains \<^latex>\<open>xxx\<close> blocks? In the past (\<^raw>) I had the idea that they don't count at all, but I don't know where I got that impression from. Empirically they do seem to be counted - maybe roughly the length of xxx?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.