src/HOL/Tools/inductive_package.ML
changeset 18145 6757627acf59
parent 17985 d5d576b72371
child 18222 a8ccacce3b52
equal deleted inserted replaced
18144:4edcb5fdc3b0 18145:6757627acf59