src/Doc/Prog_Prove/Logic.thy
 changeset 68800 d4bad1efa268 parent 67613 ce654b0e6d69 child 69505 cc2d676d5395
equal inserted replaced
   121 \end{center}
   121 \end{center}
   122 The ASCII forms of @{text"\<Union>"} are \texttt{\char\\\char\<Union>} and \texttt{Union},
   122 The ASCII forms of @{text"\<Union>"} are \texttt{\char\\\char\<Union>} and \texttt{Union},
   123 those of @{text"\<Inter>"} are \texttt{\char\\\char\<Inter>} and \texttt{Inter}.
   123 those of @{text"\<Inter>"} are \texttt{\char\\\char\<Inter>} and \texttt{Inter}.
   124 There are also indexed unions and intersections:
   124 There are also indexed unions and intersections:
   125 \begin{center}
   125 \begin{center}
   126 @{thm UNION_eq} \\ @{thm INTER_eq}
   126 @{thm[eta_contract=false] UNION_eq} \\ @{thm[eta_contract=false] INTER_eq}
   127 \end{center}
   127 \end{center}
   128 The ASCII forms are \ \texttt{UN x:A.~B} \ and \ \texttt{INT x:A. B} \
   128 The ASCII forms are \ \texttt{UN x:A.~B} \ and \ \texttt{INT x:A. B} \
   129 where \texttt{x} may occur in \texttt{B}.
   129 where \texttt{x} may occur in \texttt{B}.
   130 If \texttt{A} is \texttt{UNIV} you can write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}.
   130 If \texttt{A} is \texttt{UNIV} you can write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}.
   131
   131