src/HOL/Inductive.thy
changeset 22320 d5260836d662
parent 22218 30a8890d2967
child 22783 e5f947e0ade8