src/HOL/Nonstandard_Analysis/document/root.tex
author wenzelm
Mon, 21 Jul 2025 16:21:37 +0200
changeset 82892 45107da819fc
parent 73404 299f6a8faccc
permissions -rw-r--r--
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 64435
diff changeset
     2
\usepackage[T1]{fontenc}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 27468
diff changeset
     3
\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
64435
c93b0e6131c3 misc tuning and modernization;
wenzelm
parents: 63590
diff changeset
     4
\usepackage{amsmath,amssymb}
63590
4854f7ee0987 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
wenzelm
parents: 62479
diff changeset
     5
\usepackage{stmaryrd}
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     6
\usepackage{pdfsetup}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     7
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     8
\urlstyle{rm}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     9
\isabellestyle{it}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    10
\pagestyle{myheadings}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    11
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    12
\begin{document}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    13
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    14
\title{Isabelle/HOL-NSA --- Non-Standard Analysis}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    15
\maketitle
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    16
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    17
\tableofcontents
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    18
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    19
\begin{center}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    20
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    21
\end{center}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    22
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    23
\newpage
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    24
58878
f962e42e324d modernized header;
wenzelm
parents: 40945
diff changeset
    25
\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    26
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    27
\parindent 0pt\parskip 0.5ex
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    28
\input{session}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    29
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    30
\end{document}