src/HOL/Library/Extended_Real.thy
changeset 65573 0f3fdf689bf9
parent 64272 f76b6dda2e56
child 65680 378a2f11bec9
equal deleted inserted replaced
65572:6acb28e5ba41 65573:0f3fdf689bf9