src/HOL/Inductive.thy
changeset 54492 6fae4ecd4ab3
parent 54398 100c0eaf63d5
child 54615 62fb5af93fe2