src/HOL/Inductive.thy
changeset 25913 e1b6521c1f94
parent 25557 ea6b11021e79
child 26013 8764a1f1253b