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