--- 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
*)
--- 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
*)
--- 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)
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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.