src/Doc/Main/Main_Doc.thy

 
 
 \section*{Lattices}
 
 Classes semilattice, lattice, distributive lattice and complete lattice (the
-latter in theory @{theory Set}).
+latter in theory @{theory HOL.Set}).
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
 @{const Lattices.inf} & @{typeof Lattices.inf}\\
 @{const Lattices.sup} & @{typeof Lattices.sup}\\
 @{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\

 @{term inv} & @{term[source]"inv_into UNIV"}
 \end{tabular}
 
 \section*{Fixed Points}
 
-Theory: @{theory Inductive}.
+Theory: @{theory HOL.Inductive}.
 
 Least and greatest fixed points in a complete lattice @{typ 'a}:
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
 @{const Inductive.lfp} & @{typeof Inductive.lfp}\\

 \end{tabular}
 
 
 \section*{Algebra}
 
-Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory
-Divides} define a large collection of classes describing common algebraic
+Theories @{theory HOL.Groups}, @{theory HOL.Rings}, @{theory HOL.Fields} and @{theory
+HOL.Divides} define a large collection of classes describing common algebraic
 structures from semigroups up to fields. Everything is done in terms of
 overloaded operators:
 
 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
 \<open>0\<close> & @{typeof zero}\\

 @{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
 @{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
 \end{supertabular}
 
 
-\section*{Set\_Interval} % @{theory Set_Interval}
+\section*{Set\_Interval} % @{theory HOL.Set_Interval}
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
 @{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
 @{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
 @{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\