src/HOL/Library/Float.thy
changeset 72566 831f17da1aab
parent 71036 dfcc1882d05a
child 72607 feebdaa346e5