# HG changeset patch
# User wenzelm
# Date 1025787783 -7200
# Node ID ca2e9b2734728941e551e223124ae2d8bcd6ae32
# Parent  5e2016d151bdbd97d6bc62755b494581319ec64b
document setup;

diff -r 5e2016d151bd -r ca2e9b273472 src/ZF/Constructible/WFrec.thy
--- 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) <->
diff -r 5e2016d151bd -r ca2e9b273472 src/ZF/Constructible/Wellorderings.thy
--- 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));
diff -r 5e2016d151bd -r ca2e9b273472 src/ZF/Constructible/document/root.tex
--- /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}