src/HOL/Record.thy
changeset 34272 95df5e6dd41c
parent 34151 8d57ce46b3f7
child 35132 d137efecf793
equal deleted inserted replaced
34271:70af06abb13d 34272:95df5e6dd41c