src/HOL/ROOT
changeset 70660 373d95cf1b98
parent 70646 a4d265a6c5cc
child 70669 abdf3732f6f1
equal deleted inserted replaced
70659:44588e355ca8 70660:373d95cf1b98
   324   description "
   324   description "
   325     Author: Clemens Ballarin, started 24 September 1999, and many others
   325     Author: Clemens Ballarin, started 24 September 1999, and many others
   326 
   326 
   327     The Isabelle Algebraic Library.
   327     The Isabelle Algebraic Library.
   328   "
   328   "
       
   329   sessions
       
   330     "HOL-Cardinals"
   329   theories
   331   theories
   330     (* Orders and Lattices *)
   332     (* Orders and Lattices *)
   331     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
   333     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
   332     (* Groups *)
   334     (* Groups *)
   333     FiniteProduct        (* Product operator for commutative groups *)
   335     FiniteProduct        (* Product operator for commutative groups *)