src/HOL/Tools/inductive.ML
changeset 79974 f0150bc6fea5
parent 79732 a53287d9add3
child 80636 4041e7c8059d
equal deleted inserted replaced
79970:773b99044329 79974:f0150bc6fea5