src/HOL/Inductive.thy
changeset 45931 99cf6e470816
parent 45907 4b41967bd77e
child 46008 c296c75f4cf4