src/HOL/Induct/Comb.ML
changeset 5191 8ceaa19f7717
parent 5148 74919e8f221c
child 5223 4cb05273f764