# HG changeset patch
# User wenzelm
# Date 1504891367 -7200
# Node ID 383d8e388d1b08058712199ef58756788929a9ab
# Parent  db317febaf0bef2c5ac5ad0164aeae3b7b1c7db5
tuned headers;

diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_commands.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_display.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_model.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_problem.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_translate.ML
--- 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
 
diff -r db317febaf0b -r 383d8e388d1b src/HOL/Tools/Nunchaku/nunchaku_util.ML
--- 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