src/HOL/Library/BigO.thy
changeset 76545 cee207c2ddec
parent 68406 6beb45f6cf67
child 76786 50672d2d78db
equal deleted inserted replaced
76544:b10926dbb763 76545:cee207c2ddec