src/HOL/Library/Indicator_Function.thy
changeset 77221 0cdb384bf56a
parent 75087 f3fcc7c5a0db
equal deleted inserted replaced
77200:8f2e6186408f 77221:0cdb384bf56a