equal
deleted
inserted
replaced
227 of \emph{respectfulness} and \emph{preservation} from Homeier |
227 of \emph{respectfulness} and \emph{preservation} from Homeier |
228 \cite{Homeier05}. |
228 \cite{Homeier05}. |
229 |
229 |
230 We will also address the criticism by Paulson \cite{Paulson06} cited at the |
230 We will also address the criticism by Paulson \cite{Paulson06} cited at the |
231 beginning of this section about having to collect theorems that are lifted from the raw |
231 beginning of this section about having to collect theorems that are lifted from the raw |
232 level to the quotient level. Our quotient package id the first one that is modular so that it |
232 level to the quotient level. Our quotient package is the first one that is modular so that it |
233 allows to lift single theorems separately. This has the advantage for the |
233 allows to lift single theorems separately. This has the advantage for the |
234 user to develop a formal theory interactively an a natural progression. A |
234 user to develop a formal theory interactively an a natural progression. A |
235 pleasing result of the modularity is also that we are able to clearly |
235 pleasing result of the modularity is also that we are able to clearly |
236 specify what needs to be done in the lifting process (this was only hinted at in |
236 specify what needs to be done in the lifting process (this was only hinted at in |
237 \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code). |
237 \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code). |