src/HOL/Tools/inductive.ML
changeset 40973 890fefa597af
parent 40902 7c652e4a924a
child 41075 4bed56dc95fb
equal deleted inserted replaced
40972:ce78ef6a909b 40973:890fefa597af