equal
deleted
inserted
replaced
37 |
37 |
38 * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad, |
38 * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad, |
39 Gray and Kramer) |
39 Gray and Kramer) |
40 |
40 |
41 * ZF/Constructible: Gödel's proof of the relative consistency of the axiom |
41 * ZF/Constructible: Gödel's proof of the relative consistency of the axiom |
42 of choice is mechanized using Isabelle/ZF, following, Kunen's famous |
42 of choice is mechanized using Isabelle/ZF, following Kunen's well-known |
43 textbook "Set Theory". (Paulson) |
43 textbook "Set Theory". (Paulson) |
44 |
44 |
45 You may get Isabelle2003 from any of the following mirror sites: |
45 You may get Isabelle2003 from the following mirror sites: |
46 |
46 |
47 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
47 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
48 Munich (Germany) http://isabelle.in.tum.de/dist/ |
48 Munich (Germany) http://isabelle.in.tum.de/dist/ |