src/HOL/Algebra/document/root.bib
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 67299 ba52a058942f
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     1
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     2
@PhdThesis{Ballarin:1999,
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     3
  author = 	 {Clemens Ballarin},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     4
  title = 	 {Computer Algebra and Theorem Proving},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     5
  school = 	 {University of Cambridge},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     6
  year = 	 1999,
51516
237190475d79 Remove obsolete URLs in documentation of HOL-Algebra.
ballarin
parents: 14706
diff changeset
     7
  note =	 {Also Computer Laboratory Technical Report number 473.}
14706
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     8
}
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
     9
67299
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    10
@Misc{conrad-cyclicity,
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    11
  author = {Keith Conrad},
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    12
  title = {CYCLICITY OF {$(Z/(p))^x$}},
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    13
  howpublished = {Expository paper from the author's website},
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    14
  note = {\url{http://www.math.uconn.edu/~kconrad/blurbs/grouptheory/cyclicFp.pdf}},
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    15
}
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    16
14706
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    17
@Book{Jacobson:1985,
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    18
  author =	 {Nathan Jacobson},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    19
  title = 	 {Basic Algebra I},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    20
  publisher = 	 {Freeman},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    21
  year = 	 1985
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    22
}
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    23
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    24
@Article{Kammueller-Paulson:1999,
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    25
  author = 	 {Florian Kamm\"uller and L. C. Paulson},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    26
  title =        {A Formal Proof of Sylow's theorem: An Experiment in
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    27
                  Abstract Algebra with {Isabelle HOL}},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    28
  journal = 	 {J. Automated Reasoning},
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    29
  year = 	 1999,
67299
ba52a058942f prefer formal citations;
wenzelm
parents: 51516
diff changeset
    30
  volume =	 23,
14706
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    31
  pages =	 {235--264}
71590b7733b7 tuned document;
wenzelm
parents:
diff changeset
    32
}