--- a/src/ZF/Constructible/WFrec.thy Thu Jul 04 11:13:56 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Thu Jul 04 15:03:03 2002 +0200
@@ -113,7 +113,7 @@
apply (blast intro!: is_recfun_equal dest: transM)
done
-text{*Tells us that is_recfun can (in principle) be relativized.*}
+text{*Tells us that @{text is_recfun} can (in principle) be relativized.*}
lemma (in M_axioms) is_recfun_relativize:
"[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
==> is_recfun(r,a,H,f) <->
@@ -347,7 +347,7 @@
-text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
+text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*}
lemma (in M_ord_arith) is_oadd_fun_iff:
"[| a\<le>j; M(i); M(j); M(a); M(f) |]
==> is_oadd_fun(M,i,j,a,f) <->
--- a/src/ZF/Constructible/Wellorderings.thy Thu Jul 04 11:13:56 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Thu Jul 04 15:03:03 2002 +0200
@@ -295,7 +295,7 @@
text{*Surely a shorter proof using lemmas in @{text Order}?
- Like well_ord_iso_preserving?*}
+ Like @{text well_ord_iso_preserving}?*}
lemma (in M_axioms) ord_iso_pred_imp_lt:
"[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/document/root.tex Thu Jul 04 15:03:03 2002 +0200
@@ -0,0 +1,40 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also isabellesym.sty)
+%\usepackage{latexsym}
+%\usepackage{amssymb}
+%\usepackage[english]{babel}
+%\usepackage[latin1]{inputenc}
+%\usepackage[only,bigsqcap]{stmaryrd}
+%\usepackage{wasysym}
+%\usepackage{eufrak}
+%\usepackage{textcomp}
+%\usepackage{marvosym}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% proper setup for best-style documents
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Constructible}
+\author{Lawrence C Paulson}
+\maketitle
+
+\tableofcontents
+
+\parindent 0pt\parskip 0.5ex
+
+% include generated text of all theories
+\input{session}
+
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}