equal
deleted
inserted
replaced
544 \begin{ttbox} |
544 \begin{ttbox} |
545 consts and,or :: "gate" |
545 consts and,or :: "gate" |
546 negate :: "signal => signal" |
546 negate :: "signal => signal" |
547 \end{ttbox} |
547 \end{ttbox} |
548 |
548 |
549 \subsection{Infix and Mixfix operators} |
549 \subsection{Infix and mixfix operators} |
550 \index{infixes}\index{examples!of theories} |
550 \index{infixes}\index{examples!of theories} |
551 |
551 |
552 Infix or mixfix syntax may be attached to constants. Consider the |
552 Infix or mixfix syntax may be attached to constants. Consider the |
553 following theory: |
553 following theory: |
554 \begin{ttbox} |
554 \begin{ttbox} |
673 declaring certain types to be of class $arith$. For example, let us |
673 declaring certain types to be of class $arith$. For example, let us |
674 declare the 0-place type constructors $bool$ and $nat$: |
674 declare the 0-place type constructors $bool$ and $nat$: |
675 \index{examples!of theories} |
675 \index{examples!of theories} |
676 \begin{ttbox} |
676 \begin{ttbox} |
677 BoolNat = Arith + |
677 BoolNat = Arith + |
678 types bool,nat |
678 types bool nat |
679 arities bool,nat :: arith |
679 arities bool, nat :: arith |
680 consts Suc :: "nat=>nat" |
680 consts Suc :: "nat=>nat" |
681 \ttbreak |
681 \ttbreak |
682 rules add0 "0 + n = n::nat" |
682 rules add0 "0 + n = n::nat" |
683 addS "Suc(m)+n = Suc(m+n)" |
683 addS "Suc(m)+n = Suc(m+n)" |
684 nat1 "1 = Suc(0)" |
684 nat1 "1 = Suc(0)" |