src/HOL/Induct/LFilter.ML
changeset 5553 ae42b36a50c2
parent 5223 4cb05273f764
child 5618 721671c68324
equal deleted inserted replaced
5552:dcd3e7711cac 5553:ae42b36a50c2