with_path ".." use_thy "HOL4Compat"; with_path ".." use_thy "HOL4Syntax"; use_thy "GenHOL4Prob"; use_thy "GenHOL4Vec"; use_thy "GenHOL4Word32";