src/HOL/Import/HOL4/Generated/HOL4Real.thy
changeset 47258 880e587eee9f
parent 46787 3d3d8f8929a7