# HG changeset patch
# User wenzelm
# Date 950037156 -3600
# Node ID 67d9d52b0b725b1479d045dfd1772e1485aa39f7
# Parent  985c876b777ebddb2395ff630f2e79dc5aa94dc8
omit Primes;

diff -r 985c876b777e -r 67d9d52b0b72 src/HOL/Isar_examples/document/root.tex
--- a/src/HOL/Isar_examples/document/root.tex	Mon Feb 07 18:42:47 2000 +0100
+++ b/src/HOL/Isar_examples/document/root.tex	Tue Feb 08 20:12:36 2000 +0100
@@ -31,7 +31,6 @@
 \input{MutilatedCheckerboard.tex}
 \input{MultisetOrder.tex}
 \input{W_correct.tex}
-\input{Primes.tex}
 \input{Fibonacci.tex}
 \input{Puzzle.tex}