2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:13 +0100] rev 64587
standardized notation
src/HOL/Algebra/Coset.thy src/HOL/Algebra/Divisibility.thy src/HOL/Library/DAList_Multiset.thy src/HOL/Library/Multiset.thy src/HOL/Library/Multiset_Order.thy src/HOL/Library/Permutation.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:00 +0100] rev 64586
redundant
src/HOL/Library/Multiset.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:00 +0100] rev 64585
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
src/HOL/Library/Multiset.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:00 +0100] rev 64584
added lemmas demanded by FIXMEs
src/HOL/Relation.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:00 +0100] rev 64583
dropped comment after conversation with author: predicate compiler works independently from any code generator setup
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

2016-12-17 wenzelm [Sat, 17 Dec 2016 14:47:41 +0100] rev 64582
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
src/HOL/Library/code_test.ML src/HOL/ROOT

2016-12-17 wenzelm [Sat, 17 Dec 2016 14:13:15 +0100] rev 64581
tuned signature -- suppress pointless exports;
src/HOL/Library/code_test.ML

2016-12-17 wenzelm [Sat, 17 Dec 2016 14:09:39 +0100] rev 64580
tuned;
src/HOL/Library/code_test.ML

2016-12-17 wenzelm [Sat, 17 Dec 2016 14:04:05 +0100] rev 64579
more standard pretty printing;
tuned messages;
src/HOL/Library/code_test.ML

2016-12-17 wenzelm [Sat, 17 Dec 2016 13:42:25 +0100] rev 64578
tuned;
src/HOL/Library/Code_Test.thy src/HOL/Library/code_test.ML