src/HOL/Library/Quotient_Option.thy
changeset 59445 2c27c3d1fd3b
parent 58916 229765cc3414
child 60500 903bb1495239
equal deleted inserted replaced
59444:d57e275b2d82 59445:2c27c3d1fd3b