Hello,

I'm trying to write a lyx layout for the zed-cm style (see
ftp://ftp.comlab.ox.ac.uk/pub/CSP/LaTeX/zed-cm.sty) for writing formal
specifications of software system in the Z notation. The notation is based on
various types of boxes containing definitions of types, constants state or
state transitions. There are tools which read latex code in the correct
format and type-check the specification.

A box could f.ex. be de written as:

    \begin{axdef}
        TIME \\
        \leq : TIME \rel TIME \\
        PERIOD : \power \power_1 TIME \\
        forever : PERIOD
    \where
        \forall p \subset TIME @ \\
        \t1 [ p \in PERIOD ] \iff \\
        \t1 [ \forall a,b \in p; c \in TIME @ c \in p \iff a \leq c \land c \leq b ] \\
        forever = TIME
    \end{axdef}

The problem when I want to create a lyx layout for this environment is that
opening the environment implies a "$$" to enter math mode. I suppose I could
modify the style to remove this and then manuall enter math mode inside the
box, but that would break the type-checking.

Then, of course, there are all sorts fo things I don't know how to do, since
this is my first layout, but as far as I can see, the implied math mode can't
be defined. Please tell me how I'm wrong :)

Oh, and a quick latex quiestion, since I'm writing anyway. How do I stack
symbols? I want to write the string "inf" over the symbol \leftrightarrow
to specify an infix operator.

-- 
Logi Ragnarsson - [EMAIL PROTECTED] - [EMAIL PROTECTED]
Some day we all shall be out of scope

Reply via email to