src/HOL/Algebra/document/root.bib

more uniform operations wrt. Thm.full_prop_of;

@PhdThesis{Ballarin:1999,
  author = 	 {Clemens Ballarin},
  title = 	 {Computer Algebra and Theorem Proving},
  school = 	 {University of Cambridge},
  year = 	 1999,
  note =	 {Also Computer Laboratory Technical Report number 473.}
}

@Misc{conrad-cyclicity,
  author = {Keith Conrad},
  title = {CYCLICITY OF {$(Z/(p))^x$}},
  howpublished = {Expository paper from the author's website},
  note = {\url{http://www.math.uconn.edu/~kconrad/blurbs/grouptheory/cyclicFp.pdf}},
}

@Book{Jacobson:1985,
  author =	 {Nathan Jacobson},
  title = 	 {Basic Algebra I},
  publisher = 	 {Freeman},
  year = 	 1985
}

@Article{Kammueller-Paulson:1999,
  author = 	 {Florian Kamm\"uller and L. C. Paulson},
  title =        {A Formal Proof of Sylow's theorem: An Experiment in
                  Abstract Algebra with {Isabelle HOL}},
  journal = 	 {J. Automated Reasoning},
  year = 	 1999,
  volume =	 23,
  pages =	 {235--264}
}