{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:41:00Z","timestamp":1770298860619,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540221647","type":"print"},{"value":"9783540248491","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_3","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"34-50","source":"Crossref","is-referenced-by-count":47,"title":["Locales and Locale Expressions in Isabelle\/Isar"],"prefix":"10.1007","author":[{"given":"Clemens","family":"Ballarin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","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: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 38\u201342. Springer, Heidelberg (2000)"},{"key":"3_CR2","unstructured":"Bailey, A.: The machine-checked literate formalisation of algebra in type theory. PhD thesis, University of Manchester (January 1998)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrzaszcz","year":"2003","unstructured":"Chrzaszcz, J.: Implementing modules in the Coq system. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/10721959_7","volume-title":"Automated Deduction - CADE-17","author":"F. Kamm\u00fcller","year":"2000","unstructured":"Kamm\u00fcller, F.: Modular reasoning in Isabelle. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 99\u2013114. Springer, Heidelberg (2000)"},{"key":"3_CR5","unstructured":"Klein, G.: Verified Java Bytecode Verification. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","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, pp. 259\u2013278. Springer, Heidelberg (2003)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: 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_CR8","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002), Electronically published as \n                  \n                    http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html"},{"key":"3_CR9","unstructured":"Wenzel, M.: Using locales in Isabelle\/Isar. Part of the Isabelle2003 distribution, file src\/HOL\/ex\/Locales.thy. Distribution of Isabelle (2002), available at \n                  \n                    http:\/\/isabelle.in.tum.de"},{"key":"3_CR10","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual. Part of the Isabelle2003 distribution (2003), available at \n                  \n                    http:\/\/isabelle.in.tum.de"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:15:15Z","timestamp":1620011715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}