src/HOL/Inductive.thy
changeset 11364 01020b10c0a7
parent 11325 a5e0289dd56c
child 11436 3f74b80d979f