--- a/doc-src/Inductive/ind-defs.tex Fri Nov 21 11:57:58 1997 +0100
+++ b/doc-src/Inductive/ind-defs.tex Fri Nov 21 12:14:47 1997 +0100
@@ -1,3 +1,4 @@
+%% $Id$
\documentclass[12pt]{article}
\usepackage{a4,latexsym,../iman,../extra,../proof}
@@ -18,13 +19,9 @@
\newcommand\sbs{\subseteq}
\let\To=\Rightarrow
-%\newcommand\emph[1]{{\em#1\/}}
\newcommand\defn[1]{{\bf#1}}
-%\newcommand\textsc[1]{{\sc#1}}
-%\newcommand\texttt[1]{{\tt#1}}
\newcommand\pow{{\cal P}}
-%%%\let\pow=\wp
\newcommand\RepFun{\hbox{\tt RepFun}}
\newcommand\cons{\hbox{\tt cons}}
\def\succ{\hbox{\tt succ}}