@InProceedings{ManoliosVroon03a,
 author       = {Panagiotis Manolios and Daron Vroon},
 title        = {Ordinal Arithmetic in {ACL2}},
 editor       = {Matt Kaufmann and J Strother Moore},
 booktitle    = {Fourth International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2}-2003)},
 title        = {Fourth International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2}-2003)},
 month        = "July",
 year         = "2003",
 note         = "See URL \html{http://\-www.cs.\-utexas.edu/\-users/\-moore/\-acl2/\-workshop-2003/}"
}