# HG changeset patch
# User paulson
# Date 966936264 -7200
# Node ID 4a3c49420efdacacc59f1222f96e696c8dfabab4
# Parent  0fe0dce56bd8204aa68d1f3bf19c24b582a90e37
removed most "makeatother", no longer needed

diff -r 0fe0dce56bd8 -r 4a3c49420efd doc-src/Tutorial/fp.tex
--- a/doc-src/Tutorial/fp.tex	Tue Aug 22 10:59:15 2000 +0200
+++ b/doc-src/Tutorial/fp.tex	Tue Aug 22 11:24:24 2000 +0200
@@ -1079,7 +1079,7 @@
 \ttbreak
 set trace_simp;
 by(Simp_tac 1);
-\ttbreak\makeatother
+\ttbreak
 \Out{ Applying instance of rewrite rule:}
 \Out{ rev (?x # ?xs) == rev ?xs @ [?x]}
 \Out{ Rewriting:}
@@ -1089,7 +1089,7 @@
 \Out{ rev [] == []}
 \Out{ Rewriting:}
 \Out{ rev [] == []}
-\ttbreak\makeatother
+\ttbreak
 \Out{ Applying instance of rewrite rule:}
 \Out{ [] @ ?y == ?y}
 \Out{ Rewriting:}
@@ -1158,8 +1158,8 @@
 \begin{ttbox}
 \input{Misc/itrev1.ML}\end{ttbox}
 There is no choice as to the induction variable, and we immediately simplify:
-\begin{ttbox}
-\input{Misc/induct_auto.ML}\ttbreak\makeatother
+\begin{ttbox}\makeatother
+\input{Misc/induct_auto.ML}\ttbreak
 \Out{ 1. !!a list. itrev list [] = rev list\(\;\)==> itrev list [a] = rev list @ [a]}
 \end{ttbox}
 Just as predicted above, the overall goal, and hence the induction