src/HOL/Inductive.thy
changeset 45932 6f08f8fe9752
parent 45907 4b41967bd77e
child 46008 c296c75f4cf4