src/HOL/Library/Indicator_Function.thy
changeset 63325 1086d56cde86
parent 63309 a77adb28a27a
child 63649 e690d6f2185b