--- a/src/HOL/Analysis/Simplex_Content.thy Fri Oct 15 18:09:34 2021 +0200
+++ b/src/HOL/Analysis/Simplex_Content.thy Tue Oct 19 16:10:36 2021 +0200
@@ -1,6 +1,6 @@
(*
File: Analysis/Simplex_Content.thy
- Author: Manuel Eberl <eberlm@in.tum.de>
+ Author: Manuel Eberl <manuel@pruvisto.org>
The content of an n-dimensional simplex, including the formula for the content of a
triangle and Heron's formula.
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy Fri Oct 15 18:09:34 2021 +0200
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Tue Oct 19 16:10:36 2021 +0200
@@ -1,6 +1,6 @@
(*
File: HOL/Computational_Algebra/Nth_Powers.thy
- Author: Manuel Eberl <eberlm@in.tum.de>
+ Author: Manuel Eberl <manuel@pruvisto.org>
n-th powers in general and n-th roots of natural numbers
*)
--- a/src/HOL/Computational_Algebra/Squarefree.thy Fri Oct 15 18:09:34 2021 +0200
+++ b/src/HOL/Computational_Algebra/Squarefree.thy Tue Oct 19 16:10:36 2021 +0200
@@ -1,6 +1,6 @@
(*
File: HOL/Computational_Algebra/Squarefree.thy
- Author: Manuel Eberl <eberlm@in.tum.de>
+ Author: Manuel Eberl <manuel@pruvisto.org>
Squarefreeness and decomposition of ring elements into square part and squarefree part
*)
--- a/src/HOL/Library/Landau_Symbols.thy Fri Oct 15 18:09:34 2021 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Tue Oct 19 16:10:36 2021 +0200
@@ -1,6 +1,6 @@
(*
File: Landau_Symbols_Definition.thy
- Author: Manuel Eberl <eberlm@in.tum.de>
+ Author: Manuel Eberl <manuel@pruvisto.org>
Landau symbols for reasoning about the asymptotic growth of functions.
*)
--- a/src/HOL/Number_Theory/Prime_Powers.thy Fri Oct 15 18:09:34 2021 +0200
+++ b/src/HOL/Number_Theory/Prime_Powers.thy Tue Oct 19 16:10:36 2021 +0200
@@ -1,6 +1,6 @@
(*
File: HOL/Number_Theory/Prime_Powers.thy
- Author: Manuel Eberl <eberlm@in.tum.de>
+ Author: Manuel Eberl <manuel@pruvisto.org>
Prime powers and the Mangoldt function
*)