summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/ZF/ZF.tex

changeset 6592 | c120262044b6 |

parent 6173 | 2c0579e8e6fa |

child 6745 | 74e8f703f5f2 |

--- a/doc-src/ZF/ZF.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/ZF/ZF.tex Wed May 05 16:44:42 1999 +0200 @@ -31,7 +31,7 @@ Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF} less formally than this chapter. Isabelle employs a novel treatment of non-well-founded data structures within the standard {\sc zf} axioms including -the Axiom of Foundation~\cite{paulson-final}. +the Axiom of Foundation~\cite{paulson-mscs}. \section{Which version of axiomatic set theory?} @@ -1116,7 +1116,7 @@ non-standard notion of disjoint sum using non-standard pairs. All of these concepts satisfy the same properties as their standard counterparts; in addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive -definitions, for example of infinite lists~\cite{paulson-final}. +definitions, for example of infinite lists~\cite{paulson-mscs}. \begin{figure} \begin{ttbox} @@ -2386,10 +2386,10 @@ induction. \item Theory \texttt{ListN} inductively defines the lists of $n$ - elements~\cite{paulin92}. + elements~\cite{paulin-tlca}. \item Theory \texttt{Acc} inductively defines the accessible part of a - relation~\cite{paulin92}. + relation~\cite{paulin-tlca}. \item Theory \texttt{Comb} defines the datatype of combinators and inductively defines contraction and parallel contraction. It goes on to