equal
deleted
inserted
replaced
268 Title = {A Logic Program for Transforming Sequent Proofs to Natural |
268 Title = {A Logic Program for Transforming Sequent Proofs to Natural |
269 Deduction Proofs}, |
269 Deduction Proofs}, |
270 crossref = {extensions91}, |
270 crossref = {extensions91}, |
271 pages = {157-178}} |
271 pages = {157-178}} |
272 |
272 |
|
273 @Article{fleuriot-jcm, |
|
274 author = {Jacques Fleuriot and Lawrence C. Paulson}, |
|
275 title = {Mechanizing Nonstandard Real Analysis}, |
|
276 journal = {LMS Journal of Computation and Mathematics}, |
|
277 year = 2000, |
|
278 volume = 3, |
|
279 pages = {140-190}, |
|
280 note = {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}} |
|
281 } |
|
282 |
273 @TechReport{frost93, |
283 @TechReport{frost93, |
274 author = {Jacob Frost}, |
284 author = {Jacob Frost}, |
275 title = {A Case Study of Co-induction in {Isabelle HOL}}, |
285 title = {A Case Study of Co-induction in {Isabelle HOL}}, |
276 institution = CUCL, |
286 institution = CUCL, |
277 number = 308, |
287 number = 308, |