src/Doc/JEdit/JEdit.thy
changeset 78761 6b3f13d39612
parent 78659 b5f3d1051b13
child 79497 3225f823b337
equal deleted inserted replaced
78760:6ca807f7fed0 78761:6b3f13d39612