src/HOL/Library/Quotient_Option.thy
changeset 55456 a422f93eae0d
parent 53026 e1a548c11845
child 55466 786edc984c98