src/HOL/Library/BigO.thy
changeset 29270 0eade173f77e
parent 27487 c8a6ce181805
child 29667 53103fc8ffa3