tuned headers;
authorwenzelm
Fri, 08 Sep 2017 19:22:47 +0200
changeset 66646 383d8e388d1b
parent 66645 db317febaf0b
child 66647 6666fced78cc
tuned headers;
src/HOL/Tools/Nunchaku/nunchaku.ML
src/HOL/Tools/Nunchaku/nunchaku_collect.ML
src/HOL/Tools/Nunchaku/nunchaku_commands.ML
src/HOL/Tools/Nunchaku/nunchaku_display.ML
src/HOL/Tools/Nunchaku/nunchaku_model.ML
src/HOL/Tools/Nunchaku/nunchaku_problem.ML
src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
src/HOL/Tools/Nunchaku/nunchaku_tool.ML
src/HOL/Tools/Nunchaku/nunchaku_translate.ML
src/HOL/Tools/Nunchaku/nunchaku_util.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
 
--- 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