src/HOL/Inductive.thy
changeset 26310 f8a7fac36e13
parent 26013 8764a1f1253b
child 26793 e36a92ff543e