minimal document;
authorwenzelm
Sun Feb 09 17:47:23 2014 +0100 (2014-02-09)
changeset 55370e6be866b5f5b
parent 55369 713629c2b73c
child 55371 cb0c6cb10681
minimal document;
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/document/root.tex
src/HOL/ROOT
     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sun Feb 09 17:41:17 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sun Feb 09 17:47:23 2014 +0100
     1.3 @@ -668,7 +668,7 @@
     1.4  
     1.5  subsection{*Prime factorizations*}
     1.6  
     1.7 -text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*}
     1.8 +(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
     1.9  
    1.10  definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Number_Theory/document/root.tex	Sun Feb 09 17:47:23 2014 +0100
     2.3 @@ -0,0 +1,28 @@
     2.4 +\documentclass[11pt,a4paper]{article}
     2.5 +\usepackage{graphicx}
     2.6 +\usepackage{isabelle,isabellesym}
     2.7 +\usepackage{pdfsetup}
     2.8 +
     2.9 +\urlstyle{rm}
    2.10 +\isabellestyle{it}
    2.11 +
    2.12 +
    2.13 +\begin{document}
    2.14 +
    2.15 +\title{Various results of number theory}
    2.16 +\maketitle
    2.17 +
    2.18 +\tableofcontents
    2.19 +
    2.20 +\begin{center}
    2.21 +  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
    2.22 +\end{center}
    2.23 +
    2.24 +\newpage
    2.25 +
    2.26 +\parindent 0pt\parskip 0.5ex
    2.27 +
    2.28 +\input{session}
    2.29 +
    2.30 +\end{document}
    2.31 +
     3.1 --- a/src/HOL/ROOT	Sun Feb 09 17:41:17 2014 +0100
     3.2 +++ b/src/HOL/ROOT	Sun Feb 09 17:47:23 2014 +0100
     3.3 @@ -184,6 +184,8 @@
     3.4    theories
     3.5      Pocklington
     3.6      Number_Theory
     3.7 +  files
     3.8 +    "document/root.tex"
     3.9  
    3.10  session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
    3.11    description {*