{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:37Z","timestamp":1751660497713},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540140313"},{"type":"electronic","value":"9783540391852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_15","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T20:13:43Z","timestamp":1193429623000},"page":"259-278","source":"Crossref","is-referenced-by-count":28,"title":["Structured Proofs in Isar\/HOL"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Gertrud Bauer and Markus Wenzel. Calculational reasoning revisited \u2014 an Isabelle\/Isar experience. In R. Boulton and P. Jackson, editors, Theorem Proving in Higher Order Logics, TPHOLs 2001, volume 2152 of Lect. Notes in Comp. Sci., pages 75\u201390. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44755-5_7"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"M.C.J. Gordon, Robin Milner, and C.P. Wadsworth. Edinburgh LCF: a Mechanised Logic of Computation, volume 78 of Lect. Notes in Comp. Sci. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Florian Kamm\u00fcller, Markus Wenzel, and Lawrence C. Paulson. Locales: A sectioning concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, TPHOLs\u201999, volume 1690 of Lect. Notes in Comp. Sci., pages 149\u2013165. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48256-3_11"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic, volume 2283 of Lect. Notes in Comp. Sci. Springer-Verlag, 2002. http:\/\/www.in.tum.de\/~ nipkow\/LNCS2283\/ .","DOI":"10.1007\/3-540-45949-9"},{"key":"15_CR5","unstructured":"P. Rudnicki. An overview of the Mizar project. In Workshop on Types for Proofs and Programs. Chalmers University of Technology, 1992."},{"key":"15_CR6","unstructured":"Markus Wenzel. Isabelle\/Isar \u2014 A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 2002. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html ."},{"key":"15_CR7","unstructured":"Markus Wenzel. The Isabelle\/Isar Reference Manual. Technische Universit\u00e4t M\u00fcnchen, 2002. http:\/\/isabelle.in.tum.de\/dist\/Isabelle2002\/doc\/isar-ref.pdf ."},{"key":"15_CR8","unstructured":"Markus Wenzel and Freek Wiedijk. A comparison of the mathematical proof languages Mizar and Isar. J. Automated Reasoning, 2003. To appear."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T01:48:45Z","timestamp":1556934525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}