src/HOL/Inductive.thy
changeset 59698 d4ce901f20c5
parent 58889 5b7a9633cfa8
child 60173 6a61bb577d5b
equal deleted inserted replaced
59697:43e14b0e2ef8 59698:d4ce901f20c5