{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T01:49:47Z","timestamp":1768009787631,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540488156","type":"print"},{"value":"9783540488163","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11921240_19","type":"book-chapter","created":{"date-parts":[[2006,11,2]],"date-time":"2006-11-02T08:28:19Z","timestamp":1162456099000},"page":"272-286","source":"Crossref","is-referenced-by-count":17,"title":["Partizan Games in Isabelle\/HOLZF"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Conway, J.H.: On Numbers And Games, 2nd edn. A K Peters Ltd. (2001)","DOI":"10.1201\/9781439864159"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11617990_11","volume-title":"Types for Proofs and Programs","author":"L.E. Mamane","year":"2006","unstructured":"Mamane, L.E.: Surreal Numbers in Coq. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 170\u2013185. Springer, Heidelberg (2006)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","first-page":"190","volume-title":"Theorem Proving in Higher Order Logics","author":"M.J.C. Gordon","year":"1996","unstructured":"Gordon, M.J.C.: Set Theory, Higher Order Logic or Both. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 190\u2013201. Springer, Heidelberg (1996)"},{"key":"19_CR4","unstructured":"Agerholm, S.: Formalising a Model of the \u03bb-Calculus in HOL-ST. Technical Report 354, University of Cambridge Computer Laboratory (1994)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Agerholm, S., Gordon, M.J.C.: Experiments with ZF Set Theory in HOL and Isabelle. Technical Report RS-95-37, BRICS (1995)","DOI":"10.7146\/brics.v2i37.19940"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Automated Reasoning\u00a011, 353\u2013389 (1993)","journal-title":"J. Automated Reasoning"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L.C. Paulson","year":"1995","unstructured":"Paulson, L.C.: Set theory for verification: II. Induction and Recursion. J. Automated Reasoning\u00a015, 167\u2013215 (1995)","journal-title":"J. Automated Reasoning"},{"key":"19_CR8","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: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That, Cambridge U.P (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"19_CR10","volume-title":"Set Theory","author":"T. Jech","year":"2003","unstructured":"Jech, T.: Set Theory, 3rd rev. edn. Springer, Heidelberg (2003)","edition":"3"},{"issue":"1","key":"19_CR11","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/s10817-004-3997-6","volume":"33","author":"L.C. Paulson","year":"2004","unstructured":"Paulson, L.C.: Organizing Numerical Theories Using Axiomatic Type Classes. Journal of Automated Reasoning\u00a033(1), 29\u201349 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Defining Functions on Equivalence Classes. In: ACM Transactions on Computational Logic (in press)","DOI":"10.1145\/1183278.1183280"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/11541868_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Obua","year":"2005","unstructured":"Obua, S.: Proving bounds for real linear programs in isabelle\/HOL. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 227\u2013244. Springer, Heidelberg (2005)"},{"key":"19_CR14","unstructured":"Obua, S.: Partizan Games in Isabelle\/HOLZF, www4.in.tum.de\/~obua\/partizan"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11921240_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:59:00Z","timestamp":1605625140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11921240_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540488156","9783540488163"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11921240_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}