make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
session CTT = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*}
options [document = false]
theories Main
session "CTT-ex" in ex = CTT +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Examples for Constructive Type Theory.
*}
options [document = false]
theories Typechecking Elimination Equality Synthesis