No more makeatletter/other
authorpaulson
Thu, 20 Nov 1997 10:50:51 +0100
changeset 42398c98484ef66f
parent 4238 679a233fb206
child 4240 8ba60a4cd380
No more makeatletter/other
doc-src/Inductive/ind-defs.tex
doc-src/Intro/intro.tex
     1.1 --- a/doc-src/Inductive/ind-defs.tex	Tue Nov 18 16:37:25 1997 +0100
     1.2 +++ b/doc-src/Inductive/ind-defs.tex	Thu Nov 20 10:50:51 1997 +0100
     1.3 @@ -1,11 +1,5 @@
     1.4  \documentclass[12pt]{article}
     1.5 -\usepackage{a4,latexsym,proof}
     1.6 -
     1.7 -\makeatletter
     1.8 -\input{../rail.sty}
     1.9 -\input{../iman.sty}
    1.10 -\input{../extra.sty}
    1.11 -\makeatother
    1.12 +\usepackage{a4,latexsym,../iman,../extra,../proof}
    1.13  
    1.14  \newif\ifshort%''Short'' means a published version, not the documentation
    1.15  \shortfalse%%%%%\shorttrue
     2.1 --- a/doc-src/Intro/intro.tex	Tue Nov 18 16:37:25 1997 +0100
     2.2 +++ b/doc-src/Intro/intro.tex	Thu Nov 20 10:50:51 1997 +0100
     2.3 @@ -1,11 +1,5 @@
     2.4  \documentclass[12pt]{article}
     2.5 -\usepackage{a4}
     2.6 -
     2.7 -\makeatletter
     2.8 -\input{../proof.sty}
     2.9 -\input{../iman.sty}
    2.10 -\input{../extra.sty}
    2.11 -\makeatother
    2.12 +\usepackage{a4,../iman,../extra,../proof}
    2.13  
    2.14  %% $Id$
    2.15  %% run    bibtex intro         to prepare bibliography