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