src/HOL/Import/Generate-HOL/GenHOL4Real.thy
changeset 23719 ccd9cb15c062
parent 22997 d4f3b015b50b
child 23881 851c74f1bb69