make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
@ARTICLE{paulson-gr,
author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice},
journal = {Journal of Automated Reasoning},
year = {1996},
volume = {17},
number = {3},
pages = {291-323},
month = dec}
@Book{rubin&rubin,
author = {Herman Rubin and Jean E. Rubin},
title = {Equivalents of the Axiom of Choice, {II}},
publisher = "North-Holland",
year = 1985}