src/HOL/Tools/old_inductive_package.ML
changeset 22448 f982e73e36de
parent 22101 6d13239d5f52
child 22846 fb79144af9a3
equal deleted inserted replaced
22447:013dbd8234f0 22448:f982e73e36de