src/HOL/Induct/ROOT.ML
changeset 16633 208ebc9311f2
parent 15172 73069e033a0b
child 17598 7540ccd2b445
equal deleted inserted replaced
16632:ad2895beef79 16633:208ebc9311f2