Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
\begin{thebibliography}{10}
\bibitem{andrews86}
Andrews, P.~B.,
\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
Through Proof},
\newblock Academic Press, 1986
\bibitem{basin91}
Basin, D., Kaufmann, M.,
\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
Univ. Press, 1991, pp.~89--119
\bibitem{boyer86}
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
\bibitem{bm88book}
Boyer, R.~S., Moore, J.~S.,
\newblock {\em A Computational Logic Handbook},
\newblock Academic Press, 1988
\bibitem{camilleri92}
Camilleri, J., Melham, T.~F.,
\newblock Reasoning with inductively defined relations in the {HOL} theorem
prover,
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
\bibitem{charniak80}
Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
\newblock {\em Artificial Intelligence Programming},
\newblock Lawrence Erlbaum Associates, 1980
\bibitem{church40}
Church, A.,
\newblock A formulation of the simple theory of types,
\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
\bibitem{coen92}
Coen, M.~D.,
\newblock {\em Interactive Program Derivation},
\newblock PhD thesis, University of Cambridge, 1992,
\newblock Computer Laboratory Technical Report 272
\bibitem{constable86}
{Constable et al.}, R.~L.,
\newblock {\em Implementing Mathematics with the Nuprl Proof Development
System},
\newblock Prentice-Hall, 1986
\bibitem{davey&priestley}
Davey, B.~A., Priestley, H.~A.,
\newblock {\em Introduction to Lattices and Order},
\newblock Cambridge Univ. Press, 1990
\bibitem{dawson90}
Dawson, W.~M.,
\newblock {\em A Generic Logic Environment},
\newblock PhD thesis, Imperial College, London, 1990
\bibitem{debruijn72}
de~Bruijn, N.~G.,
\newblock Lambda calculus notation with nameless dummies, a tool for automatic
formula manipulation, with application to the {Church-Rosser Theorem},
\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
\bibitem{devlin79}
Devlin, K.~J.,
\newblock {\em Fundamentals of Contemporary Set Theory},
\newblock Springer, 1979
\bibitem{coq}
{Dowek et al.}, G.,
\newblock The {Coq} proof assistant user's guide,
\newblock Technical Report 134, INRIA-Rocquencourt, 1991
\bibitem{dummett}
Dummett, M.,
\newblock {\em Elements of Intuitionism},
\newblock Oxford University Press, 1977
\bibitem{dyckhoff}
Dyckhoff, R.,
\newblock Contraction-free sequent calculi for intuitionistic logic,
\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
\bibitem{felty91a}
Felty, A.,
\newblock A logic program for transforming sequent proofs to natural deduction
proofs,
\newblock In {\em Extensions of Logic Programming\/} (1991),
P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
\newblock LNAI 475
\bibitem{felty93}
Felty, A.,
\newblock Implementing tactics and tacticals in a higher-order logic
programming language,
\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
\bibitem{frost93}
Frost, J.,
\newblock A case study of co-induction in {Isabelle HOL},
\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
\bibitem{OBJ}
Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
\newblock Principles of {OBJ2},
\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
\bibitem{gallier86}
Gallier, J.~H.,
\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
Proving},
\newblock Harper \& Row, 1986
\bibitem{mgordon-hol}
Gordon, M. J.~C., Melham, T.~F.,
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
Order Logic},
\newblock Cambridge Univ. Press, 1993
\bibitem{halmos60}
Halmos, P.~R.,
\newblock {\em Naive Set Theory},
\newblock Van Nostrand, 1960
\bibitem{harper-jacm}
Harper, R., Honsell, F., Plotkin, G.,
\newblock A framework for defining logics,
\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
\bibitem{haskell-tutorial}
Hudak, P., Fasel, J.~H.,
\newblock A gentle introduction to {Haskell},
\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
\bibitem{haskell-report}
Hudak, P., Jones, S.~P., Wadler, P.,
\newblock Report on the programming language {Haskell}: A non-strict, purely
functional language,
\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
\newblock Version 1.2
\bibitem{huet75}
Huet, G.~P.,
\newblock A unification algorithm for typed $\lambda$-calculus,
\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
\bibitem{huet78}
Huet, G.~P., Lang, B.,
\newblock Proving and applying program transformations expressed with
second-order patterns,
\newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
\bibitem{mural}
Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
\newblock {\em Mural: A Formal Development Support System},
\newblock Springer, 1991
\bibitem{alf}
Magnusson, L., {Nordstr\"om}, B.,
\newblock The {ALF} proof editor and its proof engine,
\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
'93}\/} (published 1994), Springer, pp.~213--237,
\newblock LNCS 806
\bibitem{mw81}
Manna, Z., Waldinger, R.,
\newblock Deductive synthesis of the unification algorithm,
\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
\bibitem{martin-nipkow}
Martin, U., Nipkow, T.,
\newblock Ordered rewriting and confluence,
\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
Springer, pp.~366--380,
\newblock LNCS 449
\bibitem{martinlof84}
Martin-L\"of, P.,
\newblock {\em Intuitionistic type theory},
\newblock Bibliopolis, 1984
\bibitem{melham89}
Melham, T.~F.,
\newblock Automating recursive type definitions in higher order logic,
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
pp.~341--386
\bibitem{miller-mixed}
Miller, D.,
\newblock Unification under a mixed prefix,
\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
\bibitem{milner-coind}
Milner, R., Tofte, M.,
\newblock Co-induction in relational semantics,
\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
\bibitem{nipkow-prehofer}
Nipkow, T., Prehofer, C.,
\newblock Type checking type classes,
\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
\bibitem{noel}
{No\"el}, P.,
\newblock Experimenting with {Isabelle} in {ZF} set theory,
\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
\bibitem{nordstrom90}
{Nordstr\"om}, B., Petersson, K., Smith, J.,
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
\newblock Oxford University Press, 1990
\bibitem{paulin92}
Paulin-Mohring, C.,
\newblock Inductive definitions in the system {Coq}: Rules and properties,
\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
1992
\bibitem{paulson85}
Paulson, L.~C.,
\newblock Verifying the unification algorithm in {LCF},
\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
\bibitem{paulson87}
Paulson, L.~C.,
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
\newblock Cambridge Univ. Press, 1987
\bibitem{paulson89}
Paulson, L.~C.,
\newblock The foundation of a generic theorem prover,
\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
\bibitem{paulson-COLOG}
Paulson, L.~C.,
\newblock A formulation of the simple theory of types (for {Isabelle}),
\newblock In {\em COLOG-88: International Conference on Computer Logic\/}
(Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
Sciences, Springer,
\newblock LNCS 417
\bibitem{paulson700}
Paulson, L.~C.,
\newblock {Isabelle}: The next 700 theorem provers,
\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
Press, 1990, pp.~361--386
\bibitem{paulson91}
Paulson, L.~C.,
\newblock {\em {ML} for the Working Programmer},
\newblock Cambridge Univ. Press, 1991
\bibitem{paulson-coind}
Paulson, L.~C.,
\newblock Co-induction and co-recursion in higher-order logic,
\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
\bibitem{paulson-fixedpt}
Paulson, L.~C.,
\newblock A fixedpoint approach to implementing (co)inductive definitions,
\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
\bibitem{paulson-set-I}
Paulson, L.~C.,
\newblock Set theory for verification: {I}. {From} foundations to functions,
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
\bibitem{paulson-set-II}
Paulson, L.~C.,
\newblock Set theory for verification: {II}. {Induction} and recursion,
\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
\bibitem{paulson-final}
Paulson, L.~C.,
\newblock A concrete final coalgebra theorem for {ZF} set theory,
\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
\bibitem{pelletier86}
Pelletier, F.~J.,
\newblock Seventy-five problems for testing automatic theorem provers,
\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
\newblock Errata, JAR 4 (1988), 235--236
\bibitem{plaisted90}
Plaisted, D.~A.,
\newblock A sequent-style model elimination strategy and a positive refinement,
\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
\bibitem{quaife92}
Quaife, A.,
\newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
\bibitem{sawamura92}
Sawamura, H., Minami, T., Ohashi, K.,
\newblock Proof methods based on sheet of thought in {EUODHILOS},
\newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
Study of Social Information Science, Fujitsu Laboratories, 1992
\bibitem{suppes72}
Suppes, P.,
\newblock {\em Axiomatic Set Theory},
\newblock Dover, 1972
\bibitem{takeuti87}
Takeuti, G.,
\newblock {\em Proof Theory}, 2nd~ed.,
\newblock North Holland, 1987
\bibitem{thompson91}
Thompson, S.,
\newblock {\em Type Theory and Functional Programming},
\newblock Addison-Wesley, 1991
\bibitem{principia}
Whitehead, A.~N., Russell, B.,
\newblock {\em Principia Mathematica},
\newblock Cambridge Univ. Press, 1962,
\newblock Paperback edition to *56, abridged from the 2nd edition (1927)
\bibitem{wos-bledsoe}
Wos, L.,
\newblock Automated reasoning and {Bledsoe's} dream for the field,
\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
\end{thebibliography}