1.1 --- a/src/HOL/MicroJava/document/root.bib	Fri Sep 15 18:36:50 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/document/root.bib	Fri Sep 15 18:43:15 2000 +0200
     1.3 @@ -1,9 +1,8 @@
     1.4 -
     1.5  @inproceedings{NipkowOP00,
     1.6          author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
     1.7          title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
     1.8          booktitle = {Foundations of Secure Computation},
     1.9 -        series= {NATO Science Series F: Computer and Systems Sciences}
    1.10 +        series= {NATO Science Series F: Computer and Systems Sciences},
    1.11          volume = {175},
    1.12          year = {2000},
    1.13          publisher = {IOS Press},
    1.14 @@ -29,13 +28,13 @@
    1.15  
    1.16  @inproceedings{DvO-ECOOP00,
    1.17          author = {David von Oheimb},
    1.18 -        title = {Axiomatic Semantics for Java_light in Isabelle/HOL},
    1.19 +        title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in {Isabelle/HOL}},
    1.20          booktitle = {Formal Techniques for {J}ava Programs},
    1.21          year = {2000},
    1.22          publisher = {Fernuniversit{{\"a}t} Hagen},
    1.23          editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
    1.24          organization = {Technical Report 269, 5/2000, Fernuniversit{{\"a}t} Hagen},
    1.25 -        note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}}
    1.26 +        note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
    1.27          abstract = {We introduce a Hoare-style calculus for a nearly 
    1.28  full subset of sequential Java, which we call Java_light. In particular, 
    1.29  we present solutions to challenging features like exception handling, 
    1.30 @@ -64,6 +63,6 @@
    1.31          publisher = {Fernuniversit{{\"a}t} Hagen},
    1.32          editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
    1.33          organization = {Technical Report 269, 5/2000, Fernuniversit{{\"a}t} Hagen},
    1.34 -        note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}}
    1.35 +        note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
    1.36          url       = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
    1.37  }