# HG changeset patch
# User wenzelm
# Date 1215108906 -7200
# Node ID c686f9abc99c40ca69e9ec4ef1b0a65d9b11a1cc
# Parent  0e47e4a68709fff992aad38242afec8604a384a6
removed old NSPrimes, cf. NSA/Examples/;

diff -r 0e47e4a68709 -r c686f9abc99c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Jul 03 20:10:52 2008 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jul 03 20:15:06 2008 +0200
@@ -98,7 +98,6 @@
   "../Complex/ex/BinEx",
   "../Complex/ex/Sqrt",
   "../Complex/ex/Sqrt_Script",
-  "../Complex/ex/NSPrimes",
   "../Complex/ex/BigO_Complex",
 
   "../Complex/ex/Arithmetic_Series_Complex",