src/HOL/cladata.ML
changeset 3718 d78cf498a88c
parent 3615 e5322197cfea
child 3842 b55686a7b22c
equal deleted inserted replaced
3717:e28553315355 3718:d78cf498a88c