src/HOL/Inductive.thy
changeset 26582 6f9c62d17baa
parent 26013 8764a1f1253b
child 26793 e36a92ff543e