src/HOL/Library/Option_ord.thy
changeset 63413 9fe2d9dc095e
parent 62343 24106dc44def
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
63412:def97df48390 63413:9fe2d9dc095e