remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
(* Author: Clemens Ballarin, started 24 September 1999
The Isabelle Algebraic Library.
*)
(* Preliminaries from set and number theory *)
no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
(*** New development, based on explicit structures ***)
use_thys [
(* Groups *)
"FiniteProduct", (* Product operator for commutative groups *)
"Sylow", (* Sylow's theorem *)
"Bij", (* Automorphism Groups *)
(* Rings *)
"Divisibility", (* Rings *)
"IntRing", (* Ideals and residue classes *)
"UnivPoly" (* Polynomials *)
];
(*** Old development, based on axiomatic type classes ***)
no_document use_thys [
"abstract/Abstract", (*The ring theory*)
"poly/Polynomial" (*The full theory*)
];