src/HOL/Tools/inductive_package.ML
changeset 16240 95cc0e8f8a17
parent 16122 864fda4a4056
child 16287 7a03b4b4df67
equal deleted inserted replaced
16239:5be516f79075 16240:95cc0e8f8a17