src/HOL/Import/Generate-HOL/GenHOL4Real.thy
changeset 29163 e72d07a878f8
parent 24996 ebd5f4cc7118
child 34974 18b41bba42b5