197 isabelle.control-reset.label=Control reset |
197 isabelle.control-reset.label=Control reset |
198 isabelle.control-reset.shortcut=C+e LEFT |
198 isabelle.control-reset.shortcut=C+e LEFT |
199 isabelle.decrease-font-size.label=Decrease font size |
199 isabelle.decrease-font-size.label=Decrease font size |
200 isabelle.decrease-font-size.shortcut2=C+SUBTRACT |
200 isabelle.decrease-font-size.shortcut2=C+SUBTRACT |
201 isabelle.decrease-font-size.shortcut=C+MINUS |
201 isabelle.decrease-font-size.shortcut=C+MINUS |
|
202 isabelle.decrease-font-size2.label=Decrease font size (clone) |
|
203 #isabelle.decrease-font-size2.shortcut2=C+SUBTRACT |
|
204 #isabelle.decrease-font-size2.shortcut=C+MINUS |
202 isabelle.increase-font-size.label=Increase font size |
205 isabelle.increase-font-size.label=Increase font size |
203 isabelle.increase-font-size.shortcut2=C+ADD |
206 isabelle.increase-font-size.shortcut2=C+ADD |
204 isabelle.increase-font-size.shortcut=C+PLUS |
207 isabelle.increase-font-size.shortcut=C+PLUS |
|
208 isabelle.increase-font-size2.label=Increase font size (clone) |
|
209 #isabelle.increase-font-size2.shortcut2=C+ADD |
|
210 isabelle.increase-font-size2.shortcut=C+EQUALS |
205 lang.usedefaultlocale=false |
211 lang.usedefaultlocale=false |
206 largefilemode=full |
212 largefilemode=full |
207 line-end.shortcut=END |
213 line-end.shortcut=END |
208 line-home.shortcut=HOME |
214 line-home.shortcut=HOME |
209 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel |
215 lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel |