2015-11-19 wenzelm [Thu, 19 Nov 2015 22:06:14 +0100] rev 61705
trim lines for @{theory_text} similarly to @{text};
src/Pure/General/symbol_pos.ML src/Pure/Thy/document_antiquotations.ML

2015-11-19 wenzelm [Thu, 19 Nov 2015 20:55:40 +0100] rev 61704
tuned;
src/Pure/Thy/document_antiquotations.ML

2015-11-19 nipkow [Thu, 19 Nov 2015 18:43:41 +0100] rev 61703
tuned and converted to cmp
src/HOL/Data_Structures/Tree234.thy src/HOL/Data_Structures/Tree234_Set.thy

2015-11-19 Lars Hupel <lars.hupel@mytum.de> [Thu, 19 Nov 2015 10:05:46 +0100] rev 61702
misc. changes to Imperative-HOL from Peter Gammie
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy src/HOL/Imperative_HOL/ex/List_Sublist.thy src/HOL/Imperative_HOL/ex/Subarray.thy src/HOL/Imperative_HOL/ex/Sublist.thy

2015-11-18 ballarin [Wed, 18 Nov 2015 21:18:33 +0100] rev 61701
Refine the supression of abbreviations for morphisms that are not identities.
NEWS src/Doc/Locales/Examples1.thy src/Doc/Locales/Examples3.thy src/FOL/ex/Locale_Test/Locale_Test1.thy src/Pure/Isar/generic_target.ML

2015-11-18 paulson <lp15@cam.ac.uk> [Wed, 18 Nov 2015 17:37:00 +0000] rev 61700
Merge

2015-11-18 paulson <lp15@cam.ac.uk> [Wed, 18 Nov 2015 15:23:34 +0000] rev 61699
New theorems mostly from Peter Gammie
src/HOL/Fun.thy src/HOL/Library/Permutation.thy src/HOL/List.thy src/HOL/Multivariate_Analysis/Path_Connected.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Orderings.thy

2015-11-18 wenzelm [Wed, 18 Nov 2015 14:28:45 +0100] rev 61698
make SML/NJ happy;
src/Pure/Isar/interpretation.ML

2015-11-18 nipkow [Wed, 18 Nov 2015 10:12:37 +0100] rev 61697
converted to cmp
src/HOL/Data_Structures/Splay_Set.thy src/HOL/Data_Structures/document/root.bib src/HOL/Data_Structures/document/root.tex

2015-11-18 nipkow [Wed, 18 Nov 2015 08:54:58 +0100] rev 61696
moved lemmas
src/HOL/Data_Structures/AList_Upd_Del.thy src/HOL/Data_Structures/List_Ins_Del.thy src/HOL/Data_Structures/Sorted_Less.thy src/HOL/Data_Structures/Splay_Map.thy src/HOL/Data_Structures/Splay_Set.thy