163 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993. |
163 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993. |
164 |
164 |
165 \bibitem{paulson-CADE} |
165 \bibitem{paulson-CADE} |
166 Lawrence~C. Paulson. |
166 Lawrence~C. Paulson. |
167 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
167 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
168 \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12}, LNAI |
168 \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 |
169 814, pages 148--161. Springer, 1994. |
169 International Conference}, LNAI 814, pages 148--161. Springer, 1994. |
170 \newblock 12th international conference. |
|
171 |
170 |
172 \bibitem{paulson-set-II} |
171 \bibitem{paulson-set-II} |
173 Lawrence~C. Paulson. |
172 Lawrence~C. Paulson. |
174 \newblock Set theory for verification: {II}. {Induction} and recursion. |
173 \newblock Set theory for verification: {II}. {Induction} and recursion. |
175 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995. |
174 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995. |
176 |
175 |
177 \bibitem{paulson-coind} |
176 \bibitem{paulson-coind} |
178 Lawrence~C. Paulson. |
177 Lawrence~C. Paulson. |
179 \newblock Mechanizing coinduction and corecursion in higher-order logic. |
178 \newblock Mechanizing coinduction and corecursion in higher-order logic. |
180 \newblock {\em Journal of Logic and Computation}, 1996. |
179 \newblock {\em Journal of Logic and Computation}, 7(2), March 1997. |
181 \newblock In press. |
180 \newblock In press. |
182 |
181 |
183 \bibitem{paulson-COLOG} |
182 \bibitem{paulson-COLOG} |
184 Lawrence~C. Paulson. |
183 Lawrence~C. Paulson. |
185 \newblock A formulation of the simple theory of types (for {Isabelle}). |
184 \newblock A formulation of the simple theory of types (for {Isabelle}). |