src/HOL/Real.thy
changeset 29249 4dc278c8dc59
parent 29026 5fbaa05f637f
child 29108 12ca66b887a0