src/HOL/Inductive.thy
changeset 25577 d739f48ef40c
parent 25557 ea6b11021e79
child 26013 8764a1f1253b