src/HOL/Library/Indicator_Function.thy
changeset 77509 3bc49507bae5
parent 75087 f3fcc7c5a0db
equal deleted inserted replaced
77508:7d13996ffecc 77509:3bc49507bae5