# HG changeset patch
# User wenzelm
# Date 1334318426 -7200
# Node ID 26315a545e26b449a4e6ecb4ba918e8b622c9096
# Parent  479b4d6b9562e007816b092efb880bc7e99f0031
updated headers;

diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient3_List.thy
+(*  Title:      HOL/Library/Quotient_List.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient3_Option.thy
+(*  Title:      HOL/Library/Quotient_Option.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient3_Product.thy
+(*  Title:      HOL/Library/Quotient_Product.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient3_Set.thy
+(*  Title:      HOL/Library/Quotient_Set.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient3_Sum.thy
+(*  Title:      HOL/Library/Quotient_Sum.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      RBT_Impl.thy
+(*  Title:      HOL/Library/RBT_Impl.thy
     Author:     Markus Reiter, TU Muenchen
     Author:     Alexander Krauss, TU Muenchen
 *)
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/ComputeFloat.thy
+(*  Title:      HOL/Matrix_LP/ComputeFloat.thy
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
--- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
     Author:     Steven Obua, TU Munich
 
 Steven Obua's evaluator.
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/am_compiler.ML
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/am_ghc.ML
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_ghc.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/am_interpreter.ML
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/am_sml.ML
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_sml.ML
     Author:     Steven Obua
 
 TODO: "parameterless rewrite cannot be used in pattern": In a lot of
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/compute.ML
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/compute.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Compute_Oracle/linker.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Compute_Oracle/linker.ML
+(*  Title:      HOL/Matrix_LP/Compute_Oracle/linker.ML
     Author:     Steven Obua
 
 This module solves the problem that the computing oracle does not
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Cplex.thy
--- a/src/HOL/Matrix_LP/Cplex.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Cplex.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Cplex.thy
+(*  Title:      HOL/Matrix_LP/Cplex.thy
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/CplexMatrixConverter.ML
--- a/src/HOL/Matrix_LP/CplexMatrixConverter.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/CplexMatrixConverter.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/CplexMatrixConverter.ML
+(*  Title:      HOL/Matrix_LP/CplexMatrixConverter.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Cplex_tools.ML
+(*  Title:      HOL/Matrix_LP/Cplex_tools.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/FloatSparseMatrixBuilder.ML
+(*  Title:      HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/LP.thy
--- a/src/HOL/Matrix_LP/LP.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/LP.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/LP.thy
+(*  Title:      HOL/Matrix_LP/LP.thy
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/Matrix.thy
+(*  Title:      HOL/Matrix_LP/Matrix.thy
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/SparseMatrix.thy
--- a/src/HOL/Matrix_LP/SparseMatrix.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/SparseMatrix.thy
+(*  Title:      HOL/Matrix_LP/SparseMatrix.thy
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/fspmlp.ML
--- a/src/HOL/Matrix_LP/fspmlp.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/fspmlp.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/fspmlp.ML
+(*  Title:      HOL/Matrix_LP/fspmlp.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Matrix_LP/matrixlp.ML
--- a/src/HOL/Matrix_LP/matrixlp.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Matrix_LP/matrixlp.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Matrix/matrixlp.ML
+(*  Title:      HOL/Matrix_LP/matrixlp.ML
     Author:     Steven Obua
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Quotient3_Examples/FSet.thy
+(*  Title:      HOL/Quotient_Examples/FSet.thy
     Author:     Cezary Kaliszyk, TU Munich
     Author:     Christian Urban, TU Munich
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Apr 13 14:00:26 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Quotient3_Examples/Lift_Fun.thy
+(*  Title:      HOL/Quotient_Examples/Lift_Fun.thy
     Author:     Ondrej Kuncar
 *)
 
diff -r 479b4d6b9562 -r 26315a545e26 src/HOL/Tools/legacy_transfer.ML
--- a/src/HOL/Tools/legacy_transfer.ML	Fri Apr 13 13:59:35 2012 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML	Fri Apr 13 14:00:26 2012 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/Tools/transfer.ML
+(*  Title:      HOL/Tools/legacy_transfer.ML
     Author:     Amine Chaieb, University of Cambridge, 2009
-                Jeremy Avigad, Carnegie Mellon University
-                Florian Haftmann, TU Muenchen
+    Author:     Jeremy Avigad, Carnegie Mellon University
+    Author:     Florian Haftmann, TU Muenchen
 
 Simple transfer principle on theorems.
 *)