{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T11:53:51Z","timestamp":1773143631552,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_21","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"279-294","source":"Crossref","is-referenced-by-count":51,"title":["Type Classes and Filters for Mathematical Analysis in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Johannes","family":"H\u00f6lzl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabian","family":"Immler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Huffman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1112\/S1461157000000267","volume":"3","author":"J.D. Fleuriot","year":"2000","unstructured":"Fleuriot, J.D., Paulson, L.C.: Mechanizing nonstandard real analysis. LMS Journal of Computation and Mathematics\u00a03, 140\u2013190 (2000)","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive Type Classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 160\u2013174. Springer, Heidelberg (2007)"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-02444-3_10","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2009","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 153\u2013168. Springer, Heidelberg (2009)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J.V. Harrison","year":"2005","unstructured":"Harrison, J.V.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J. H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 135\u2013151. Springer, Heidelberg (2011)"},{"key":"21_CR6","unstructured":"Immler, F.: Generic construction of probability spaces for paths of stochastic processes in Isabelle\/HOL. Master\u2019s thesis, TU M\u00fcnchen (October 2012)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-32347-8_26","volume-title":"Interactive Theorem Proving","author":"F. Immler","year":"2012","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 377\u2013392. Springer, Heidelberg (2012)"},{"key":"21_CR8","unstructured":"Joshi, K.D.: Introduction to General Topology. John Wiley and Sons (1983)"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Lester, D.R.: Topology in PVS: continuous mathematics with applications. In: Second Workshop on Automated Formal Methods, AFM 2007, pp. 11\u201320 (2007)","DOI":"10.1145\/1345169.1345171"},{"key":"21_CR10","first-page":"1","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. MSCS, Interactive theorem proving and the form. of math.\u00a021, 1\u201331 (2011)","journal-title":"MSCS, Interactive theorem proving and the form. of math."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T22:21:40Z","timestamp":1557958900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}