src/HOL/Library/Indicator_Function.thy
changeset 80645 a1dce0cc6c26
parent 75087 f3fcc7c5a0db
equal deleted inserted replaced
80644:6a996ad11af2 80645:a1dce0cc6c26