{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T12:07:10Z","timestamp":1791029230797,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":4,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540672821","type":"print"},{"value":"9783540464198","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_3","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T19:17:25Z","timestamp":1186600645000},"page":"38-43","source":"Crossref","is-referenced-by-count":65,"title":["Proof General: A Generic Tool for Proof Development"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"3_CR1","unstructured":"D. Aspinall, H. Goguen, T. Kleymann, and D. Sequira. Proof General. System documentation, see \n                    http:\/\/www.dcs.ed.ac.uk\/home\/proofgen\n                    \n                  , 1999. 41"},{"key":"3_CR2","unstructured":"Yves Bertot, Thomas Kleymann, and Dilip Sequeira. Implementing proof by pointing without a structure editor. Technical Report ECS-LFCS-97-368, University of Edinburgh, 1997. 41"},{"issue":"7","key":"3_CR3","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jsco.1997.0171","volume":"25","author":"Y. Bertot","year":"1998","unstructured":"Yves Bertot and Laurent Th\u00e9ry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7):161\u2013194, February 1998. 41","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u201999","author":"M. Wenzel","year":"1999","unstructured":"Markus Wenzel. Isar \u2014 a generic interpretative approach to readable formal proof documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u201999, Lecture Notes in Computer Science 1690. Springer-Verlag, 1999. 40"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T00:03:20Z","timestamp":1550707400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":4,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}