# HG changeset patch
# User paulson
# Date 880019451 -3600
# Node ID 8c98484ef66f56e89b6727df83b068f7bd8ed261
# Parent  679a233fb206a0eee19f447f049cb07d7b5ad6e5
No more makeatletter/other

diff -r 679a233fb206 -r 8c98484ef66f doc-src/Inductive/ind-defs.tex
--- a/doc-src/Inductive/ind-defs.tex	Tue Nov 18 16:37:25 1997 +0100
+++ b/doc-src/Inductive/ind-defs.tex	Thu Nov 20 10:50:51 1997 +0100
@@ -1,11 +1,5 @@
 \documentclass[12pt]{article}
-\usepackage{a4,latexsym,proof}
-
-\makeatletter
-\input{../rail.sty}
-\input{../iman.sty}
-\input{../extra.sty}
-\makeatother
+\usepackage{a4,latexsym,../iman,../extra,../proof}
 
 \newif\ifshort%''Short'' means a published version, not the documentation
 \shortfalse%%%%%\shorttrue
diff -r 679a233fb206 -r 8c98484ef66f doc-src/Intro/intro.tex
--- a/doc-src/Intro/intro.tex	Tue Nov 18 16:37:25 1997 +0100
+++ b/doc-src/Intro/intro.tex	Thu Nov 20 10:50:51 1997 +0100
@@ -1,11 +1,5 @@
 \documentclass[12pt]{article}
-\usepackage{a4}
-
-\makeatletter
-\input{../proof.sty}
-\input{../iman.sty}
-\input{../extra.sty}
-\makeatother
+\usepackage{a4,../iman,../extra,../proof}
 
 %% $Id$
 %% run    bibtex intro         to prepare bibliography