src/HOL/Inductive.thy
changeset 55003 c65fd9218ea1
parent 54615 62fb5af93fe2
child 55534 b18bdcbda41b