src/HOL/Inductive.ML
changeset 4950 226f2cde9f4d
parent 4872 33e7cdc20681
child 4970 8b65444edbb0