39 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
39 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
40 mechanism for extension is the introduction of safe definitions and of |
40 mechanism for extension is the introduction of safe definitions and of |
41 non-empty types. Both extensions are often performed in quotient |
41 non-empty types. Both extensions are often performed in quotient |
42 constructions. To ease the work involved with such quotient constructions, we |
42 constructions. To ease the work involved with such quotient constructions, we |
43 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
43 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
44 extended his work in order to deal with compositions of quotients. Also, we |
44 extended his work in order to deal with compositions of quotients. We also |
45 designed our quotient package so that every step in a quotient construction |
45 designed our quotient package so that every step in a quotient construction |
46 can be performed separately and as a result we are able to specify completely |
46 can be performed separately and as a result we are able to specify completely |
47 the procedure of lifting theorems from the raw level to the quotient level. |
47 the procedure of lifting theorems from the raw level to the quotient level. |
48 The importance for programming language research is that many properties of |
48 The importance for programming language research is that many properties of |
49 programming language calculi are easier to verify over $\alpha$-equated, or |
49 programming language calculi are easier to verify over $\alpha$-equated, or |