src/HOL/Induct/LFilter.ML
changeset 5089 f95e0a6eb775
parent 5069 3ea049f7979d
child 5143 b94cd208f073
equal deleted inserted replaced
5088:e4aa78d1312f 5089:f95e0a6eb775