src/HOL/Induct/Common_Patterns.thy
changeset 67830 4f992daf4707
parent 63233 e53830948c4f