src/HOL/Inductive.thy
changeset 54838 16511f84913c
parent 54615 62fb5af93fe2
child 55534 b18bdcbda41b