equal
deleted
inserted
replaced
67 re-implemented in the popular Isabelle/HOL theorem prover the quotient |
67 re-implemented in the popular Isabelle/HOL theorem prover the quotient |
68 package by Homeier. In doing so we extended his work in order to deal with |
68 package by Homeier. In doing so we extended his work in order to deal with |
69 compositions of quotients and also specified completely the procedure |
69 compositions of quotients and also specified completely the procedure |
70 of lifting theorems from the raw level to the quotient level. |
70 of lifting theorems from the raw level to the quotient level. |
71 The importance for theorem proving is that many formal |
71 The importance for theorem proving is that many formal |
72 verifications, in order to be feasible, require a convenient resoning infrastructure |
72 verifications, in order to be feasible, require a convenient reasoning infrastructure |
73 for quotient constructions. |
73 for quotient constructions. |
74 \end{abstract} |
74 \end{abstract} |
75 |
75 |
76 %\category{D.??}{TODO}{TODO} |
76 %\category{D.??}{TODO}{TODO} |
77 |
77 |