--- a/src/HOL/Analysis/Cartesian_Space.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy Tue May 15 13:57:39 2018 +0200
@@ -1,10 +1,11 @@
-(* Title: Cartesian_Space.thy
- Author: Amine Chaieb, University of Cambridge
- Author: Jose Divasón <jose.divasonm at unirioja.es>
- Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
- Author: Johannes Hölzl, VU Amsterdam
- Author: Fabian Immler, TUM
+(* Title: HOL/Analysis/Cartesian_Space.thy
+ Author: Amine Chaieb, University of Cambridge
+ Author: Jose Divasón <jose.divasonm at unirioja.es>
+ Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
+ Author: Johannes Hölzl, VU Amsterdam
+ Author: Fabian Immler, TUM
*)
+
theory Cartesian_Space
imports
Finite_Cartesian_Product Linear_Algebra
--- a/src/HOL/Computational_Algebra/Group_Closure.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/HOL/Computational_Algebra/Group_Closure.thy Tue May 15 13:57:39 2018 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Computational_Algebra/Field_as_Ring.thy
+(* Title: HOL/Computational_Algebra/Group_Closure.thy
Author: Johannes Hoelzl, TU Muenchen
Author: Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/Hull.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/HOL/Hull.thy Tue May 15 13:57:39 2018 +0200
@@ -1,8 +1,8 @@
-(* Title: Hull.thy
- Author: Amine Chaieb, University of Cambridge
- Author: Jose Divasón <jose.divasonm at unirioja.es>
- Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
- Author: Johannes Hölzl, VU Amsterdam
+(* Title: HOL/Hull.thy
+ Author: Amine Chaieb, University of Cambridge
+ Author: Jose Divasón <jose.divasonm at unirioja.es>
+ Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
+ Author: Johannes Hölzl, VU Amsterdam
*)
theory Hull
--- a/src/HOL/Library/FuncSet.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue May 15 13:57:39 2018 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/FuncSet.thy
+(* Title: HOL/Library/FuncSet.thy
Author: Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
*)
--- a/src/HOL/Modules.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/HOL/Modules.thy Tue May 15 13:57:39 2018 +0200
@@ -1,9 +1,9 @@
-(* Title: Modules.thy
- Author: Amine Chaieb, University of Cambridge
- Author: Jose Divasón <jose.divasonm at unirioja.es>
- Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
- Author: Johannes Hölzl, VU Amsterdam
- Author: Fabian Immler, TUM
+(* Title: HOL/Modules.thy
+ Author: Amine Chaieb, University of Cambridge
+ Author: Jose Divasón <jose.divasonm at unirioja.es>
+ Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
+ Author: Johannes Hölzl, VU Amsterdam
+ Author: Fabian Immler, TUM
*)
section \<open>Modules\<close>
--- a/src/HOL/Vector_Spaces.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy Tue May 15 13:57:39 2018 +0200
@@ -1,9 +1,9 @@
-(* Title: Vector_Spaces.thy
- Author: Amine Chaieb, University of Cambridge
- Author: Jose Divasón <jose.divasonm at unirioja.es>
- Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
- Author: Johannes Hölzl, VU Amsterdam
- Author: Fabian Immler, TUM
+(* Title: HOL/Vector_Spaces.thy
+ Author: Amine Chaieb, University of Cambridge
+ Author: Jose Divasón <jose.divasonm at unirioja.es>
+ Author: Jesús Aransay <jesus-maria.aransay at unirioja.es>
+ Author: Johannes Hölzl, VU Amsterdam
+ Author: Fabian Immler, TUM
*)
section \<open>Vector Spaces\<close>
--- a/src/Pure/Sessions.thy Tue May 15 11:33:43 2018 +0200
+++ b/src/Pure/Sessions.thy Tue May 15 13:57:39 2018 +0200
@@ -1,4 +1,4 @@
-(* Title: Pure/Thy/Sessions.thy
+(* Title: Pure/Sessions.thy
Author: Makarius
PIDE markup for session ROOT.