{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:51:13Z","timestamp":1781927473881,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664635","type":"print"},{"value":"9783540482567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_12","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:15:22Z","timestamp":1186157722000},"page":"167-183","source":"Crossref","is-referenced-by-count":102,"title":["Isar \u2014 A Generic Interpretative Approach to Readable Formal Proof Documents"],"prefix":"10.1007","author":[{"given":"Markus","family":"Wenzel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"12_CR1","unstructured":"K. Arkoudas. Deduction vis-a-vis computation: The need for a formal language for proof engineering. The MIT Express project, http:\/\/www.ai.mit.edu\/projects\/express\/ , June 1998."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. Mega: Towards a mathematical assistant. In W. McCune, editor, 14th International Conference on Automated Deduction \u2014 CADE-14, volume 1249 of LNAI. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"12_CR3","unstructured":"Y. Bertot and L. Th\u00e9ry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 11, 1996."},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics","author":"R. Boulton","year":"1998","unstructured":"R. Boulton, K. Slind, A. Bundy, and M. Gordon. An interface between CLAM and HOL. In J. Grundy and M. Newey, editors, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, volume 1479 of LNCS. Springer, 1998."},{"key":"12_CR5","unstructured":"R. Burstall. Teaching people to write proofs: a tool. In CafeOBJ Symposium, Numazu, Japan, April 1998."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56\u201368, 1940.","DOI":"10.2307\/2266170"},{"key":"12_CR7","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, and C Mu\u00f1oz. The Coq Proof Assistant User\u2019s Guide, version 6.1. INRIA-Rocquencourt et CNRSENS Lyon, 1996."},{"key":"12_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Typed Lambda Calculus and Applications","author":"Y. Coscoy","year":"1995","unstructured":"Y. Coscoy, G. Kahn, and L. Th\u00e9ry. Extracting text from proofs. In Typed Lambda Calculus and Applications, volume 902 of LNCS. Springer, 1995."},{"issue":"5","key":"12_CR9","first-page":"261","volume":"30","author":"B. I. Dahn","year":"1994","unstructured":"B. I. Dahn and A. Wolf. A calculus supporting structured proofs. Journal of Information Processing and Cybernetics (EIK), 30(5\u20146):261\u2013276, 1994. Akademie Verlag Berlin.","journal-title":"Journal of Information Processing and Cybernetics (EIK)"},{"key":"12_CR10","unstructured":"M. J. C. Gordon and T. F. Melham (editors). Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"12_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201996","author":"J. Harrison","year":"1996","unstructured":"J. Harrison. A Mizar mode for HOL. In J. Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201996, volume 1125 of LNCS, pages 203\u2013220. Springer, 1996."},{"key":"12_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1007\/3-540-61511-3_125","volume-title":"13th International Conference on Automated Deduction\u2013CADE-13","author":"T. Nipkow","year":"1996","unstructured":"T. Nipkow. More Church-Rosser proofs (in Isabelle\/HOL). In M. McRobbie and J. K. Slaney, editors, 13th International Conference on Automated Deduction\u2013CADE-13, volume 1104 of LNCS, pages 733\u2013747. Springer, 1996."},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-62034-6_48","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Nipkow","year":"1996","unstructured":"T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru, editor, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of LNCS, pages 180\u2013192. Springer, 1996."},{"key":"12_CR14","first-page":"161","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"T. Nipkow and D. v. Oheimb. Javalight is type-safe \u2014 definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161\u2013170. ACM Press, New York, 1998."},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas. PVS: combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification, volume 1102 of LNCS. Springer, 1996."},{"key":"12_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994."},{"key":"12_CR17","unstructured":"L. C. Paulson. Generic automatic proof tools. In R. Veroff, editor, Automated Reasoning and its Applications. MIT Press, 1997."},{"key":"12_CR18","unstructured":"L. C. Paulson. A generic tableau prover and its integration with Isabelle. In CADE-15 Workshop on Integration of Deductive Systems, 1998."},{"key":"12_CR19","volume-title":"1992 Workshop on Types for Proofs and Programs","author":"P. Rudnicki","year":"1992","unstructured":"P. Rudnicki. An overview of the MIZAR project. In 1992 Workshop on Types for Proofs and Programs. Chalmers University of Technology, Bastad, 1992."},{"key":"12_CR20","unstructured":"D. Syme. DECLARE: A prototype declarative proof system for higher order logic. Technical Report 416, University of Cambridge Computer Laboratory, 1997."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"D. Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998. Submitted.","DOI":"10.1007\/3-540-48256-3_14"},{"key":"12_CR22","unstructured":"A. Trybulec. Some features of the Mizar language. Presented at a workshop in Turin, Italy, 1993."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T14:58:43Z","timestamp":1556722723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]}}}