src/HOL/Inductive.thy
changeset 58278 e89c7ac4ce16
parent 58187 d2ddd401d74d
child 58306 117ba6cbe414