src/HOL/Library/Indicator_Function.thy
changeset 63414 beb987127d0f
parent 63309 a77adb28a27a
child 63649 e690d6f2185b