src/HOL/Library/Quotient_Sum.thy
changeset 80484 0ca36dcdcbd3
parent 67399 eab6ce8368fa
equal deleted inserted replaced
80483:5b539d1d3577 80484:0ca36dcdcbd3