src/HOL/Import/Generate-HOL/GenHOL4Real.thy
changeset 25332 73491e84ead1
parent 24996 ebd5f4cc7118
child 34974 18b41bba42b5