Re: [isabelle] typesetting compound subscripts



Many thanks!

Part of my confusion was the difference between what happens when
Isabelle typesets constdefs at the top level of a .thy file, and what
happens when it pretty-prints quoted theorems, as in your @{thm
[display] mytest_def [no_vars]}.  At present I'm using the former, to
get some control over the layout of big formulas, and to include
comments in them.  Am I right in (now) guessing that to get the intended
typesetting I therefore have to use the verbose syntax explicitly,
e.g. something like this:

constdefs
mytest3 :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool"
"mytest3 tos n t1 t2 ==  (t1 \<le>\<^bsub> tos n \<^esub> t2)"

ie, there's no way to have the abbreviation automatically applied?

ta,
Peter








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