{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:30Z","timestamp":1774837950599,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371045","type":"print"},{"value":"9783540371069","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11812289_3","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T08:23:44Z","timestamp":1159518224000},"page":"17-30","source":"Crossref","is-referenced-by-count":7,"title":["Structured Induction Proofs in Isabelle\/Isar"],"prefix":"10.1007","author":[{"given":"Makarius","family":"Wenzel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Aspinall, D.: Proof General: A generic tool for proof development. In: European Joint Conferences on Theory and Practice of Software (ETAPS) (2000)","DOI":"10.1007\/3-540-46419-0_3"},{"key":"3_CR2","unstructured":"Barras, B., et al.: The Coq Proof Assistant Reference Manual, version 8. Inria (2006)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_7","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Bauer","year":"2001","unstructured":"Bauer, G., Wenzel, M.: Calculational reasoning revisited \u2014 an Isabelle\/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, Springer, Heidelberg (2001)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Dixon, L., Fleuriot, J.D.: A proof-centric approach to mathematical assistants. Journal of Applied Logic: Special Issue on Mathematics Assistance Systems (to appear)","DOI":"10.1016\/j.jal.2005.10.007"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Math. Zeitschrift (1935)","DOI":"10.1007\/BF01201353"},{"key":"3_CR6","unstructured":"Mizar mathematical library, http:\/\/www.mizar.org\/library\/"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_15","volume-title":"Types for Proofs and Programs","author":"T. Nipkow","year":"2003","unstructured":"Nipkow, T.: Structured proofs in Isar\/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, Springer, Heidelberg (2003)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"3_CR9","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, Academic Press, London (1990)"},{"key":"3_CR10","unstructured":"Rudnicki, P.: An overview of the MIZAR project. In: 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad (1992)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Schroeder-Heister, P.: A natural extension of natural deduction. Journal of Symbolic Logic\u00a049(4) (1984)","DOI":"10.2307\/2274279"},{"key":"3_CR12","unstructured":"Trybulec, A.: Some features of the Mizar language. Presented at a workshop in Turin (1993)"},{"key":"3_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_41","volume-title":"Automated Reasoning","author":"C. Urban","year":"2006","unstructured":"Urban, C., Berghofer, S.: A recursion combinator for nominal datatypes implemented in Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"3_CR14","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, Springer, Heidelberg (1999)"},{"key":"3_CR16","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen (2002), http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html"},{"key":"3_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11542384_8","volume-title":"The Seventeen Provers of the World","author":"M. Wenzel","year":"2006","unstructured":"Wenzel, M., Paulson, L.C.: Isabelle\/Isar. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600, Springer, Heidelberg (2006)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36469-2_15","volume-title":"Mathematical Knowledge Management","author":"F. Wiedijk","year":"2003","unstructured":"Wiedijk, F.: Comparing mathematical provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, Springer, Heidelberg (2003)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Wiedijk, F., Wenzel, M.: A comparison of the mathematical proof languages Mizar and Isar. Journal of Automated Reasoning\u00a029(3\u20134) (2002)","DOI":"10.1023\/A:1021935419355"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11812289_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:06Z","timestamp":1605644046000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11812289_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371045","9783540371069"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11812289_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}