src/Doc/Main/Main_Doc.thy
changeset 63950 cdc1e59aa513
parent 63935 aa1fe1103ab8
child 64267 b9a1486e79be
equal deleted inserted replaced
63949:e7e41db7221b 63950:cdc1e59aa513
   323 @{const times} & @{typeof times}\\
   323 @{const times} & @{typeof times}\\
   324 @{const inverse} & @{typeof inverse}\\
   324 @{const inverse} & @{typeof inverse}\\
   325 @{const divide} & @{typeof divide}\\
   325 @{const divide} & @{typeof divide}\\
   326 @{const abs} & @{typeof abs}\\
   326 @{const abs} & @{typeof abs}\\
   327 @{const sgn} & @{typeof sgn}\\
   327 @{const sgn} & @{typeof sgn}\\
   328 @{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
   328 @{const Rings.dvd} & @{typeof Rings.dvd}\\
   329 @{const Rings.divide} & @{typeof Rings.divide}\\
   329 @{const divide} & @{typeof divide}\\
   330 @{const div_class.mod} & @{typeof "div_class.mod"}\\
   330 @{const modulo} & @{typeof modulo}\\
   331 \end{supertabular}
   331 \end{supertabular}
   332 
   332 
   333 \subsubsection*{Syntax}
   333 \subsubsection*{Syntax}
   334 
   334 
   335 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   335 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}