src/HOL/Import/Generate-HOL/GenHOL4Real.thy
changeset 32738 15bb09ca0378
parent 24996 ebd5f4cc7118
child 34974 18b41bba42b5