On Fri, 20 Apr 2012, Lawrence Paulson wrote:
Cut and paste works much better with this version!
I still have to get to grips with a lot of very basic things
For me it has required 2 full weeks to retrain my fingers, after giving up
Escape-Meta-Alt-Control-Shift in summer 2007.
This is an insider joke: C-A C-X C-S
Emacs: go to start of line, then save buffer
jEdit: select whole text, cut it off, save file -- which is now empty
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
