{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:36Z","timestamp":1774837836170,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"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_4","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T04:23:44Z","timestamp":1159503824000},"page":"31-43","source":"Crossref","is-referenced-by-count":38,"title":["Interpretation of Locales in Isabelle: Theories and Proof Contexts"],"prefix":"10.1007","author":[{"given":"Clemens","family":"Ballarin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-45719-4_34","volume-title":"Algebraic Methodology and Software Technology","author":"S. Autexier","year":"2002","unstructured":"Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager Maya. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 495\u2013501. Springer, Heidelberg (2002)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi et al (eds.) [4], pp. 34\u201350","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"4_CR3","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: Managing dependencies between locales. Technical Report TUM-I0607, Technische Universit\u00e4t M\u00fcnchen (2006)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","year":"2004","unstructured":"Berardi, S., Coppo, M., Damiani, F. (eds.): TYPES 2003. LNCS, vol.\u00a03085. Springer, Heidelberg (2004)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Chrzaszcz, J.: Modules in Coq are and will be correct. In: Berardi et al.(eds.) [14], pp. 130\u2013136.","DOI":"10.1007\/978-3-540-24849-1_9"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction - CADE-11","author":"W.M. Farmer","year":"1992","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 567\u2013581. Springer, Heidelberg (1992)"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/ASE.2000.873647","volume-title":"Automated Software Engineering, ASE 2000","author":"D. Hutter","year":"2000","unstructured":"Hutter, D.: Management of change in structured verification. In: Automated Software Engineering, ASE 2000, Grenoble, France, pp. 23\u201331. IEEE Computer Society, Los Alamitos (2000)"},{"key":"4_CR8","unstructured":"Kamm\u00fcller, F.: Modular Reasoning in Isabelle. PhD thesis, University of Cambridge, Computer Laboratory, Also Technical Report No. 470 (August 1999)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 149\u2013165. Springer, Heidelberg (1999)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 64\u201374 (1993)","DOI":"10.1109\/LICS.1993.287599"},{"key":"4_CR11","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":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"4_CR13","unstructured":"Owre, S., Shankar, N.: Theory interpretation in PVS. Technical Report CSL-01-01, SRI (April 2001)"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning\u00a05(3), 363\u2013397 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR15","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual. Part of the Isabelle distribution, available at: \n                    \n                      http:\/\/isabelle.in.tum.de"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"},{"key":"4_CR17","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, Internet publication (2002), \n                    \n                      http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Structured induction proofs in Isabelle\/Isar. MKM (2006)","DOI":"10.1007\/11812289_3"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11812289_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:27:03Z","timestamp":1619494023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11812289_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371045","9783540371069"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11812289_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}