[isabelle] case in LaTeX output

Iâm seeing a case turn into a call to the datatypeâs case function in the LaTeX output
(see case-val below), but Iâd prefer it to stay as a case.

In particular, I have the following equation in a fun definition.

"E (EIf e1 e2 e3) Ï = (v1 â E e1 Ï;
                              case v1 of
                                (VNat n) â if n â 0 then E e2 Ï else E e3 Ï
                              | (VFun t) â zero)â

But itâs producing the following in the LaTeX (PDF):

E (if e1 then e2 else e3) Ï = set-bind (E e1 Ï) (case-val (În. if n   0 then E e2 Ï else E e3 Ï) (Ît. zero))

Iâm wondering if the set-bind is somehow triggering this behaviorâ Itâs the bind for a
non-determinism monad that I define as follows.

definition set_bind :: "'a M â ('a â 'b M) â 'b M" where
  "set_bind m f â { v. â v'. v' â m â v â f v' }"
declare set_bind_def[simp]

syntax "_set_bind" :: "[pttrns,'a M,'b] â 'c" ("(_ â _;//_)" 0)
translations "P â E; F" â "CONST set_bind E (ÎP. F)â

Any help is appreciated!


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