src/HOL/Library/Indicator_Function.thy
changeset 73652 d5c3eee7da74
parent 73536 5131c388a9b0
child 73928 3b76524f5a85