src/HOL/Inductive.thy
changeset 81005 7846fa2c1c1e
parent 80934 8e72f55295fd
child 81505 01f2936ec85e
equal deleted inserted replaced
81004:07ad0b407d38 81005:7846fa2c1c1e