src/HOL/Tools/Quotient/quotient_term.ML
changeset 78784 fb46520b9b7c
parent 74525 c960bfcb91db
child 80636 4041e7c8059d
equal deleted inserted replaced
78783:b78158997a28 78784:fb46520b9b7c