--- a/src/HOL/ROOT Thu Apr 06 08:33:37 2017 +0200
+++ b/src/HOL/ROOT Thu Apr 06 21:37:13 2017 +0200
@@ -32,10 +32,8 @@
theories
Library
(*conflicting type class instantiations and dependent applications*)
- Field_as_Ring
Finite_Lattice
List_lexord
- Polynomial_Factorial
Prefix_Order
Product_Lexorder
Product_Order
@@ -71,6 +69,13 @@
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
@@ -301,7 +306,7 @@
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 *)
@@ -418,7 +423,7 @@
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
@@ -635,7 +640,7 @@
options [quick_and_dirty]
theories [document = false]
"~~/src/HOL/Library/Lattice_Syntax"
- "../Number_Theory/Primes"
+ "../Computational_Algebra/Primes"
theories
Knaster_Tarski
Peirce