src/HOL/Lambda/document/root.tex
changeset 11945 1b540afebf4d
parent 11944 0594e63e6057
child 13031 3f7824dd8ddf
equal deleted inserted replaced
11944:0594e63e6057 11945:1b540afebf4d
     3 
     3 
     4 \documentclass[11pt,a4paper]{article}
     4 \documentclass[11pt,a4paper]{article}
     5 \usepackage{graphicx}
     5 \usepackage{graphicx}
     6 \usepackage[english]{babel}
     6 \usepackage[english]{babel}
     7 \usepackage[latin1]{inputenc}
     7 \usepackage[latin1]{inputenc}
       
     8 \usepackage{amssymb}
     8 \usepackage{isabelle,isabellesym,pdfsetup}
     9 \usepackage{isabelle,isabellesym,pdfsetup}
     9 
    10 
    10 \isabellestyle{it}
    11 \isabellestyle{it}
    11 \renewcommand{\isamarkupsubsubsection}[1]{\subsubsection*{#1}}
    12 \renewcommand{\isamarkupsubsubsection}[1]{\subsubsection*{#1}}
       
    13 \newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}}
    12 
    14 
    13 \begin{document}
    15 \begin{document}
    14 
    16 
    15 \title{Fundamental Properties of Lambda-calculus}
    17 \title{Fundamental Properties of Lambda-calculus}
    16 \author{Tobias Nipkow \\ Stefan Berghofer}
    18 \author{Tobias Nipkow \\ Stefan Berghofer}