Changes

Summary

fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
tuned whitespace;
proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;
updated to jedit-5.6pre1 (repository version 25349);

Changeset 71935:82b00b8f1871 by paulson _lp15@cam.ac.uk_: fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/Relation.thy` (diff)
The file was modified	`src/HOL/Wellfounded.thy` (diff)
Changeset 71934:914baafb3da4 by wenzelm: tuned whitespace;
The file was modified	`src/HOL/Examples/ML.thy` (diff)
The file was modified	`src/HOL/Examples/Seq.thy` (diff)
The file was modified	`src/Tools/SML/Examples.thy` (diff)
Changeset 71933:aec0f7b58cc6 by wenzelm: proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;
The file was modified	`src/Pure/General/codepoint.scala` (diff)
The file was modified	`src/Tools/jEdit/src/token_markup.scala` (diff)
Changeset 71932:65fd0f032a75 by wenzelm: updated to jedit-5.6pre1 (repository version 25349);
The file was modified	`Admin/components/components.sha1` (diff)
The file was modified	`Admin/components/main` (diff)
The file was modified	`NEWS` (diff)
The file was modified	`src/Pure/Admin/build_release.scala` (diff)
The file was modified	`src/Tools/jEdit/lib/Tools/jedit` (diff)
The file was modified	`src/Tools/jEdit/patches/accelerator_font` (diff)
The file was modified	`src/Tools/jEdit/patches/docking` (diff)
The file was modified	`src/Tools/jEdit/patches/extended_styles` (diff)
The file was modified	`src/Tools/jEdit/patches/folding` (diff)
The file was modified	`src/Tools/jEdit/patches/props` (diff)
The file was modified	`src/Tools/jEdit/patches/putenv` (diff)
The file was modified	`src/Tools/jEdit/patches/title` (diff)
The file was modified	`src/Tools/jEdit/patches/vfs_manager` (diff)
The file was modified	`src/Tools/jEdit/patches/vfs_marker` (diff)
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala` (diff)
The file was removed	`src/Tools/jEdit/patches/brackets`
The file was removed	`src/Tools/jEdit/patches/favorites`
The file was removed	`src/Tools/jEdit/patches/glyphvector`
The file was removed	`src/Tools/jEdit/patches/macosx`