src/HOL/Import/HOL/HOL4Real.thy
changeset 24546 c90cee3163b7
parent 20485 3078fd2eec7b
child 25919 8b1c0d434824