src/HOL/Library/OptionalSugar.thy
changeset 61378 3e04c9ca001a
parent 61143 5f898411ce87
child 61645 ae5e55d03e45
equal deleted inserted replaced
61377:517feb558c77 61378:3e04c9ca001a