src/HOL/ROOT
changeset 64282 261d42f0bfac
parent 64015 c9f3a94cb825
child 64323 20d15328b248
--- a/src/HOL/ROOT	Tue Oct 18 07:04:08 2016 +0200
+++ b/src/HOL/ROOT	Mon Oct 17 15:20:06 2016 +0200
@@ -218,27 +218,6 @@
   document_files
     "root.tex"
 
-session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
-  description {*
-    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
-    Theorem, Wilson's Theorem, Quadratic Reciprocity.
-  *}
-  theories [document = false]
-    "~~/src/HOL/Library/Infinite_Set"
-    "~~/src/HOL/Library/Permutation"
-  theories
-    Fib
-    Factorization
-    Chinese
-    WilsonRuss
-    WilsonBij
-    Quadratic_Reciprocity
-    Primes
-    Pocklington
-  document_files
-    "root.bib"
-    "root.tex"
-
 session "HOL-Hoare" in Hoare = HOL +
   description {*
     Verification of imperative programs (verification conditions are generated