src/HOL/Library/Confluent_Quotient.thy
changeset 79776 c3f07c950116
parent 73398 180981b87929