src/HOL/Tools/inductive.ML
changeset 53717 6eb85a1cb406
parent 52732 b4da1f2ec73f
child 53994 4237859c186d
equal deleted inserted replaced
53716:b42d9a71fc1a 53717:6eb85a1cb406