src/HOL/Inductive.thy
changeset 8450 dc44d6533f0f
parent 8343 fb604f0e5640
child 8482 bbc805ebc904
equal deleted inserted replaced
8449:f8ff23736465 8450:dc44d6533f0f