src/HOL/Library/Option_ord.thy
changeset 61247 76148d288b2e
parent 60679 ade12ef2773c
child 61955 e96292f32c3c
equal deleted inserted replaced
61246:077b88f9ec16 61247:76148d288b2e