src/HOL/Import/Generate-HOL/GenHOL4Real.thy
changeset 25656 7f4cf5b20d38
parent 24996 ebd5f4cc7118
child 34974 18b41bba42b5