equal
deleted
inserted
replaced
350 |
350 |
351 \noindent |
351 \noindent |
352 holds (for the proof see \cite{Homeier05}). |
352 holds (for the proof see \cite{Homeier05}). |
353 |
353 |
354 The next step is to lift definitions over the raw type to definitions over the |
354 The next step is to lift definitions over the raw type to definitions over the |
355 quotient type. For this we providing the declaration |
355 quotient type. For this we provide the declaration |
356 |
356 |
357 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
357 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
358 \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"} |
358 \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"} |
359 \end{isabelle} |
359 \end{isabelle} |
360 |
360 |