src/HOL/Inductive.ML
changeset 2981 aa5aeb6467c6
parent 2855 36f75c4a0047
child 3768 67f4ac759100