equal
deleted
inserted
replaced
232 @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} |
232 @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} |
233 @{thm concat.simps(2)[THEN eq_reflection, no_vars]} |
233 @{thm concat.simps(2)[THEN eq_reflection, no_vars]} |
234 \end{isabelle} |
234 \end{isabelle} |
235 |
235 |
236 \noindent |
236 \noindent |
237 We expect that the corresponding operator on finite sets, written @{term "fconcat"}, |
237 where @{text "@"} is the usual list append. We expect that the corresponding |
|
238 operator on finite sets, written @{term "fconcat"}, |
238 builds finite unions of finite sets: |
239 builds finite unions of finite sets: |
239 |
240 |
240 \begin{isabelle}\ \ \ \ \ %%% |
241 \begin{isabelle}\ \ \ \ \ %%% |
241 @{thm fconcat_empty[THEN eq_reflection, no_vars]}\hspace{10mm} |
242 @{thm fconcat_empty[THEN eq_reflection, no_vars]}\hspace{10mm} |
242 @{thm fconcat_insert[THEN eq_reflection, no_vars]} |
243 @{thm fconcat_insert[THEN eq_reflection, no_vars]} |