src/HOL/Inductive.thy
changeset 23719 ccd9cb15c062
parent 23708 b5eb0b4dd17d
child 23734 0e11b904b3a3