# HG changeset patch
# User wenzelm
# Date 1331575778 -3600
# Node ID a8b1236e0837cbda92629b8de8b704fc606ccafd
# Parent  d4fdc61d9336446778cd86efcbd4689f3aeeb6cb
tuned headers;

diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL4/Template/GenHOL4Base.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Base.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Base.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Base.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL4/Template/GenHOL4Prob.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Prob.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Prob.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Prob.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Prob.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL4/Template/GenHOL4Real.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Real.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Real.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Real.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Real.thy
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL4/Template/GenHOL4Vec.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Vec.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Vec.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Vec.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL4/Template/GenHOL4Word32.thy
--- a/src/HOL/Import/HOL4/Template/GenHOL4Word32.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL4/Template/GenHOL4Word32.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOL/GenHOL4Word32.thy
+(*  Title:      HOL/Import/HOL4/Template/GenHOL4Word32.thy
     Author:     Sebastian Skalberg, TU Muenchen
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL_Light/HOLLightInt.thy
--- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/HOLLightInt.thy
+(*  Title:      HOL/Import/HOL_Light/HOLLightInt.thy
     Author:     Cezary Kaliszyk
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL_Light/HOLLightList.thy
--- a/src/HOL/Import/HOL_Light/HOLLightList.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightList.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/HOLLightList.thy
+(*  Title:      HOL/Import/HOL_Light/HOLLightList.thy
     Author:     Cezary Kaliszyk
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL_Light/HOLLightReal.thy
--- a/src/HOL/Import/HOL_Light/HOLLightReal.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightReal.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/HOLLightReal.thy
+(*  Title:      HOL/Import/HOL_Light/HOLLightReal.thy
     Author:     Cezary Kaliszyk
 *)
 
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Import/HOL_Light/Template/GenHOLLight.thy
--- a/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
+(*  Title:      HOL/Import/HOL_Light/Template/GenHOLLight.thy
     Author:     Steven Obua, TU Muenchen
     Author:     Cezary Kaliszyk
 *)
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Quickcheck_Examples.thy
+(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
     Author:     Stefan Berghofer, Lukas Bulwahn
     Copyright   2004 - 2010 TU Muenchen
 *)
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Quickcheck_Lattice_Examples.thy
+(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
     Author:     Lukas Bulwahn
     Copyright   2010 TU Muenchen
 *)
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Quickcheck_Narrowing_Examples.thy
+(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
     Author:     Lukas Bulwahn
     Copyright   2011 TU Muenchen
 *)
diff -r d4fdc61d9336 -r a8b1236e0837 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Mar 12 16:57:29 2012 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Mar 12 19:09:38 2012 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/TPTP/?/tptp_interpret.ML
+(*  Title:      HOL/TPTP/TPTP_Parser/tptp_interpret.ML
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Interprets TPTP problems in Isabelle/HOL.