src/HOL/Induct/Com.ML
changeset 3462 3472fa00b1d4
parent 3457 a8ab7c64817c
child 3919 c036caebfc75
equal deleted inserted replaced
3461:7bf1e7c40a0c 3462:3472fa00b1d4