src/HOL/Real.thy
changeset 34309 d91c3fce478e
parent 32877 6f09346c7c08
child 35028 108662d50512
equal deleted inserted replaced
34300:3f2e25dc99ab 34309:d91c3fce478e