src/HOL/Library/Option_ord.thy
changeset 28108 1b08ed83b79e
parent 27368 9f90ac19e32b
child 28562 4e74209f113e
equal deleted inserted replaced
28107:760ecc6fc1bd 28108:1b08ed83b79e