document setup;
authorwenzelm
Thu Jul 04 15:03:03 2002 +0200 (2002-07-04)
changeset 13295ca2e9b273472
parent 13294 5e2016d151bd
child 13296 ba142aa29694
document setup;
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/Constructible/document/root.tex
     1.1 --- a/src/ZF/Constructible/WFrec.thy	Thu Jul 04 11:13:56 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WFrec.thy	Thu Jul 04 15:03:03 2002 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4  apply (blast intro!: is_recfun_equal dest: transM) 
     1.5  done 
     1.6  
     1.7 -text{*Tells us that is_recfun can (in principle) be relativized.*}
     1.8 +text{*Tells us that @{text is_recfun} can (in principle) be relativized.*}
     1.9  lemma (in M_axioms) is_recfun_relativize:
    1.10    "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    1.11     ==> is_recfun(r,a,H,f) <->
    1.12 @@ -347,7 +347,7 @@
    1.13  
    1.14  
    1.15  
    1.16 -text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
    1.17 +text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*}
    1.18  lemma (in M_ord_arith) is_oadd_fun_iff:
    1.19     "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
    1.20      ==> is_oadd_fun(M,i,j,a,f) <->
     2.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 11:13:56 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 15:03:03 2002 +0200
     2.3 @@ -295,7 +295,7 @@
     2.4  
     2.5  
     2.6  text{*Surely a shorter proof using lemmas in @{text Order}?
     2.7 -     Like well_ord_iso_preserving?*}
     2.8 +     Like @{text well_ord_iso_preserving}?*}
     2.9  lemma (in M_axioms) ord_iso_pred_imp_lt:
    2.10       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
    2.11         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Constructible/document/root.tex	Thu Jul 04 15:03:03 2002 +0200
     3.3 @@ -0,0 +1,40 @@
     3.4 +
     3.5 +\documentclass[11pt,a4paper]{article}
     3.6 +\usepackage{isabelle,isabellesym}
     3.7 +
     3.8 +% further packages required for unusual symbols (see also isabellesym.sty)
     3.9 +%\usepackage{latexsym}
    3.10 +%\usepackage{amssymb}
    3.11 +%\usepackage[english]{babel}
    3.12 +%\usepackage[latin1]{inputenc}
    3.13 +%\usepackage[only,bigsqcap]{stmaryrd}
    3.14 +%\usepackage{wasysym}
    3.15 +%\usepackage{eufrak}
    3.16 +%\usepackage{textcomp}
    3.17 +%\usepackage{marvosym}
    3.18 +
    3.19 +% this should be the last package used
    3.20 +\usepackage{pdfsetup}
    3.21 +
    3.22 +% proper setup for best-style documents
    3.23 +\urlstyle{rm}
    3.24 +\isabellestyle{it}
    3.25 +
    3.26 +
    3.27 +\begin{document}
    3.28 +
    3.29 +\title{Constructible}
    3.30 +\author{Lawrence C Paulson}
    3.31 +\maketitle
    3.32 +
    3.33 +\tableofcontents
    3.34 +
    3.35 +\parindent 0pt\parskip 0.5ex
    3.36 +
    3.37 +% include generated text of all theories
    3.38 +\input{session}
    3.39 +
    3.40 +%\bibliographystyle{abbrv}
    3.41 +%\bibliography{root}
    3.42 +
    3.43 +\end{document}