equal
deleted
inserted
replaced
364 @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
364 @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} |
365 \end{definition} |
365 \end{definition} |
366 |
366 |
367 \noindent |
367 \noindent |
368 Unfortunately, restrictions in HOL's type-system prevent us from stating |
368 Unfortunately, restrictions in HOL's type-system prevent us from stating |
369 and proving a quotient type theorem, like \ref{funquot}, for compositions |
369 and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions |
370 of relations. However, we can prove all instances where @{text R\<^isub>1} and |
370 of relations. However, we can prove all instances where @{text R\<^isub>1} and |
371 @{text "R\<^isub>2"} are built up by constituent equivalence relations. |
371 @{text "R\<^isub>2"} are built up by constituent equivalence relations. |
372 *} |
372 *} |
373 |
373 |
374 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |
374 section {* Quotient Types and Quotient Definitions\label{sec:type} *} |