tuned headers;
authorwenzelm
Mon, 12 Mar 2012 19:09:38 +0100
changeset 46879 a8b1236e0837
parent 46878 d4fdc61d9336
child 46880 af8e516953ce
tuned headers;
src/HOL/Import/HOL4/Template/GenHOL4Base.thy
src/HOL/Import/HOL4/Template/GenHOL4Prob.thy
src/HOL/Import/HOL4/Template/GenHOL4Real.thy
src/HOL/Import/HOL4/Template/GenHOL4Vec.thy
src/HOL/Import/HOL4/Template/GenHOL4Word32.thy
src/HOL/Import/HOL_Light/HOLLightInt.thy
src/HOL/Import/HOL_Light/HOLLightList.thy
src/HOL/Import/HOL_Light/HOLLightReal.thy
src/HOL/Import/HOL_Light/Template/GenHOLLight.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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.