src/HOL/Import/HOL4/Generated/one.imp
changeset 47223 4fc34c628474
parent 46787 3d3d8f8929a7