src/HOL/Induct/LFilter.ML
changeset 8800 e3688ef49f12
parent 7499 23e090051cb8
equal deleted inserted replaced
8799:89e9deef4bcb 8800:e3688ef49f12