src/HOL/Library/OptionalSugar.thy
changeset 60580 7e741e22d7fc
parent 56245 84fc7dfa3cd4
child 61143 5f898411ce87
equal deleted inserted replaced
60579:915da29bf5d9 60580:7e741e22d7fc