src/HOL/Inductive.thy
changeset 58274 4a84e94e58a2
parent 58187 d2ddd401d74d
child 58306 117ba6cbe414