src/HOL/Induct/Common_Patterns.thy
changeset 69148 d0517da45e5c
parent 63233 e53830948c4f
equal deleted inserted replaced
69147:6f4d561ea621 69148:d0517da45e5c