src/HOL/Typerep.thy
changeset 78715 9506b852ebdf
parent 74375 ba880f3a4e52
child 80760 be8c0e039a5e
equal deleted inserted replaced
78714:eb2255d241da 78715:9506b852ebdf