src/HOL/Record.thy
changeset 32497 922718ac81e4
parent 31723 f5cafe803b55
child 32743 c4e9a48bc50e
equal deleted inserted replaced
32496:4ab00a2642c3 32497:922718ac81e4