src/HOL/Inductive.thy
changeset 55456 a422f93eae0d
parent 54615 62fb5af93fe2
child 55534 b18bdcbda41b