src/HOL/RComplete.thy
changeset 41397 f5e14d6f5eba
parent 37887 2ae085b07f2f
child 41550 efa734d9b221
equal deleted inserted replaced
41396:5379e4a85a66 41397:f5e14d6f5eba