src/HOL/Examples/Records.thy
changeset 79298 77e4e69fd0e1
parent 78624 8d7394e533f8
child 80703 cc4ecaa8e96e
equal deleted inserted replaced
79286:366a5ad2f2b3 79298:77e4e69fd0e1