src/HOL/Inductive.thy
changeset 56958 b2c2f74d1c93
parent 56146 8453d35e4684
child 58112 8081087096ad