src/HOL/Inductive.thy
changeset 43460 2852f309174a
parent 43324 2b47822868e4
child 43580 023a1d1f97bd