# HG changeset patch
# User wenzelm
# Date 1491311100 -7200
# Node ID 83c30e29070217c516f7a412b7b394bcb0540ac6
# Parent  10ca63a18e56c537449eb42df916742feb497ff9
tuned headers;

diff -r 10ca63a18e56 -r 83c30e290702 src/HOL/Library/Cancellation/cancel.ML
--- a/src/HOL/Library/Cancellation/cancel.ML	Tue Apr 04 11:52:28 2017 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML	Tue Apr 04 15:05:00 2017 +0200
@@ -1,16 +1,9 @@
-(*  Title:      Provers/Arith/cancel.ML
+(*  Title:      HOL/Library/Cancellation/cancel.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Mathias Fleury, MPII
-    Copyright   2017
-
-Based on:
 
-    Title:      Provers/Arith/cancel_numerals.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
-
-
-This simproc allows handling of types with constructors (e.g., add_mset for multisets) and iteration
-of the addition (e.g., repeat_mset for multisets).
+This simproc allows handling of types with constructors (e.g., add_mset for
+multisets) and iteration of the addition (e.g., repeat_mset for multisets).
 
 Beware that this simproc should not compete with any more specialised especially:
   - nat: the handling for Suc is more complicated than what can be done here
diff -r 10ca63a18e56 -r 83c30e290702 src/HOL/Library/Cancellation/cancel_data.ML
--- a/src/HOL/Library/Cancellation/cancel_data.ML	Tue Apr 04 11:52:28 2017 +0200
+++ b/src/HOL/Library/Cancellation/cancel_data.ML	Tue Apr 04 15:05:00 2017 +0200
@@ -1,14 +1,10 @@
-(*  Title:      Provers/Arith/cancel_data.ML
+(*  Title:      HOL/Library/Cancellation/cancel_data.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Mathias Fleury, MPII
-    Copyright   2017
-
-Based on:
-    Title:      Tools/nat_numeral_simprocs.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Datastructure for the cancelation simprocs.
+*)
 
-*)
 signature CANCEL_DATA =
 sig
   val mk_sum : typ -> term list -> term
diff -r 10ca63a18e56 -r 83c30e290702 src/HOL/Library/Cancellation/cancel_simprocs.ML
--- a/src/HOL/Library/Cancellation/cancel_simprocs.ML	Tue Apr 04 11:52:28 2017 +0200
+++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML	Tue Apr 04 15:05:00 2017 +0200
@@ -1,10 +1,6 @@
-(*  Title:      Provers/Arith/cancel_simprocs.ML
+(*  Title:      HOL/Library/Cancellation/cancel_simprocs.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Mathias Fleury, MPII
-    Copyright   2017
-
-Base on:
-    Title:      Provers/Arith/nat_numeral_simprocs.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Cancelation simprocs declaration.
 *)
diff -r 10ca63a18e56 -r 83c30e290702 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Tue Apr 04 11:52:28 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala	Tue Apr 04 15:05:00 2017 +0200
@@ -1,4 +1,4 @@
-/*  Title:      Tools/jEdit/src/spell_checker.scala
+/*  Title:      Pure/Tools/spell_checker.scala
     Author:     Makarius
 
 Spell checker with completion, based on JOrtho (see
diff -r 10ca63a18e56 -r 83c30e290702 src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Tue Apr 04 11:52:28 2017 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Apr 04 15:05:00 2017 +0200
@@ -1,4 +1,4 @@
-/*  Title:      Pure/Admin/build_vscode.scala
+/*  Title:      Tools/VSCode/src/build_vscode.scala
     Author:     Makarius
 
 Build VSCode configuration and extension module for Isabelle.