equal
deleted
inserted
replaced
587 school = {University of Edinburgh}, |
587 school = {University of Edinburgh}, |
588 year = 1984} |
588 year = 1984} |
589 |
589 |
590 @article{MuellerNvOS99, |
590 @article{MuellerNvOS99, |
591 author= |
591 author= |
592 {Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch}, |
592 {Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, |
593 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}} |
593 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}} |
594 |
594 |
595 @Manual{Muzalewski:Mizar, |
595 @Manual{Muzalewski:Mizar, |
596 title = {An Outline of {PC} {Mizar}}, |
596 title = {An Outline of {PC} {Mizar}}, |
597 author = {Micha{\l} Muzalewski}, |
597 author = {Micha{\l} Muzalewski}, |
882 journal = SCP, |
882 journal = SCP, |
883 volume = 5, |
883 volume = 5, |
884 pages = {143-170}, |
884 pages = {143-170}, |
885 year = 1985} |
885 year = 1985} |
886 |
886 |
887 %replqces Paulson-LCF |
887 %replaces Paulson-LCF |
888 @book{paulson87, |
888 @book{paulson87, |
889 author = {Lawrence C. Paulson}, |
889 author = {Lawrence C. Paulson}, |
890 title = {Logic and Computation: Interactive proof with Cambridge |
890 title = {Logic and Computation: Interactive proof with Cambridge |
891 LCF}, |
891 LCF}, |
892 year = 1987, |
892 year = 1987, |