src/HOL/Tools/inductive.ML
changeset 48922 6f3ccfa7818d
parent 47876 0521ee2e504d
child 49170 03bee3a6a1b7
equal deleted inserted replaced
48921:5d8d409b897e 48922:6f3ccfa7818d