src/HOL/ROOT

     Classical Higher-order Logic -- batteries included.
   *}
   theories
     Library
     (*conflicting type class instantiations and dependent applications*)
-    Field_as_Ring
     Finite_Lattice
     List_lexord
-    Polynomial_Factorial
     Prefix_Order
     Product_Lexorder
     Product_Order
     Sublist_Order
     (*data refinements and dependent applications*)

 
 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
   theories
     Approximations
     Circle_Area
+
+session "HOL-Computation_Algebra" in "Computational_Algebra" = HOL +
+  theories
+    Computational_Algebra
+    (*conflicting type class instantiations and dependent applications*)
+    Field_as_Ring
+    Polynomial_Factorial
 
 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
   description {*
     Author:     Gertrud Bauer, TU Munich
 

     The Isabelle Algebraic Library.
   *}
   theories [document = false]
     (* Preliminaries from set and number theory *)
     "~~/src/HOL/Library/FuncSet"
-    "~~/src/HOL/Number_Theory/Primes"
+    "~~/src/HOL/Computational_Algebra/Primes"
     "~~/src/HOL/Library/Permutation"
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
 

   *}
   options [parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
-    "~~/src/HOL/Number_Theory/Primes"
+    "~~/src/HOL/Computational_Algebra/Primes"
     "~~/src/HOL/Library/State_Monad"
   theories
     Greatest_Common_Divisor
     Warshall
     Higman_Extraction

     Miscellaneous Isabelle/Isar examples.
   *}
   options [quick_and_dirty]
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
-    "../Number_Theory/Primes"
+    "../Computational_Algebra/Primes"
   theories
     Knaster_Tarski
     Peirce
     Drinker
     Cantor