src/HOL/Library/Float.thy
changeset 55456 a422f93eae0d
parent 54784 54f1ce13c140
child 55565 f663fc1e653b
equal deleted inserted replaced
55455:2cf404a469be 55456:a422f93eae0d