{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T04:04:03Z","timestamp":1725595443162},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22673-1_17","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T11:49:15Z","timestamp":1310557755000},"page":"244-259","source":"Crossref","is-referenced-by-count":18,"title":["Isabelle as Document-Oriented Proof Assistant"],"prefix":"10.1007","author":[{"given":"Makarius","family":"Wenzel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Amerkad, A., Bertot, Y., Pottier, L., Rideau, L.: Mathematics and proof presentation in Pcoq. In: Proceedings of Proof Transformation and Presentation and Proof Complexities, PTP 2001 (2001)","key":"17_CR1"},{"doi-asserted-by":"crossref","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Journal of Automated Reasoning 39(2) (2007)","key":"17_CR2","DOI":"10.1007\/s10817-007-9070-5"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A generic tool for proof development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, p. 38. Springer, Heidelberg (2000)"},{"key":"17_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-73086-6_15","volume-title":"Towards Mechanized Mathematical Assistants","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: A framework for interactive proof. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 161\u2013175. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Bertot, Y., Th\u00e9ry, L.: A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation 25(7) (1998)","key":"17_CR5","DOI":"10.1006\/jsco.1997.0171"},{"doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., Morris, L., Newey, M.C., Wadsworth, C.P.: A metalanguage for interactive proof in LCF. In: Principles of programming languages, POPL (1978)","key":"17_CR6","DOI":"10.1145\/512760.512773"},{"unstructured":"Odersky, M., et al.: An overview of the Scala programming language. Technical Report IC\/2004\/64, EPF Lausanne (2004)","key":"17_CR7"},{"doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Pretty printing. ACM Transactions on Programming Languages and Systems 2(4) (1980)","key":"17_CR8","DOI":"10.1145\/357114.357115"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-14128-7_37","volume-title":"Intelligent Computer Mathematics","author":"C. Tankink","year":"2010","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A tool for proof re-animation. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 440\u2013454. Springer, Heidelberg (2010)"},{"key":"17_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/11618027_23","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2006","unstructured":"Urban, J.: XML-izing Mizar: Making semantic processing and presentation of MML eas. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 346\u2013360. Springer, Heidelberg (2006)"},{"key":"17_CR11","series-title":"ENTCS","volume-title":"User Interfaces for Theorem Provers (UITP 2006)","author":"M. Wagner","year":"2007","unstructured":"Wagner, M., Autexier, S., Benzm\u00fcller, C.: PLAT\u03a9: A mediator between text-editors and proof assistance systems. In: Autexier, S., Benzm\u00fcller, C. (eds.) User Interfaces for Theorem Provers (UITP 2006). ENTCS, vol.\u00a0174(2). Elsevier, Amsterdam (2007)"},{"unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof \u2014 Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, vol.\u00a010(23), University of Bia\u0142ystok (2007)","key":"17_CR12"},{"unstructured":"Wenzel, M.: Asynchronous proof processing with Isabelle\/Scala and Isabelle\/jEdit. In: Sacerdoti Coen, C., Aspinall, D. (eds.) User Interfaces for Theorem Provers (UITP 2010). ENTCS (July 2010), FLOC 2010 Satellite Workshop","key":"17_CR13"},{"unstructured":"Wenzel, M.: The Isabelle\/Isar Implementation Manual (2011)","key":"17_CR14"},{"unstructured":"Wenzel, M., Chaieb, A.: SML with antiquotations embedded into Isabelle\/Isar. In: Carette, J., Wiedijk, F. (eds.) Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007), Hagenberg, Austria (June 2007)","key":"17_CR15"},{"key":"17_CR16","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T23:19:38Z","timestamp":1560381578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}