--- a/src/HOL/Tools/Nunchaku/nunchaku.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_collect.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_collect.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_commands.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_commands.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_display.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_display.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_display.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_display.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_model.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_model.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_model.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_model.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_problem.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_problem.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_problem.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_problem.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_reconstruct.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_tool.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_tool.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_translate.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_translate.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_translate.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_translate.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017
--- a/src/HOL/Tools/Nunchaku/nunchaku_util.ML Fri Sep 08 15:48:58 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_util.ML Fri Sep 08 19:22:47 2017 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Nunchaku/Tools/nunchaku_util.ML
+(* Title: HOL/Tools/Nunchaku/nunchaku_util.ML
Author: Jasmin Blanchette, VU Amsterdam
Copyright 2015, 2016, 2017