updated headers;
authorwenzelm
Fri Apr 13 14:00:26 2012 +0200 (2012-04-13)
changeset 4745526315a545e26
parent 47454 479b4d6b9562
child 47456 88adecfe4246
updated headers;
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML
src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML
src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
src/HOL/Matrix_LP/Compute_Oracle/compute.ML
src/HOL/Matrix_LP/Compute_Oracle/linker.ML
src/HOL/Matrix_LP/Cplex.thy
src/HOL/Matrix_LP/CplexMatrixConverter.ML
src/HOL/Matrix_LP/Cplex_tools.ML
src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
src/HOL/Matrix_LP/LP.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Matrix_LP/SparseMatrix.thy
src/HOL/Matrix_LP/fspmlp.ML
src/HOL/Matrix_LP/matrixlp.ML
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Lift_Fun.thy
src/HOL/Tools/legacy_transfer.ML
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Apr 13 13:59:35 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Apr 13 14:00:26 2012 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Library/Quotient3_List.thy
     1.5 +(*  Title:      HOL/Library/Quotient_List.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8  
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Apr 13 13:59:35 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Apr 13 14:00:26 2012 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Library/Quotient3_Option.thy
     2.5 +(*  Title:      HOL/Library/Quotient_Option.thy
     2.6      Author:     Cezary Kaliszyk and Christian Urban
     2.7  *)
     2.8  
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Apr 13 13:59:35 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Apr 13 14:00:26 2012 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Library/Quotient3_Product.thy
     3.5 +(*  Title:      HOL/Library/Quotient_Product.thy
     3.6      Author:     Cezary Kaliszyk and Christian Urban
     3.7  *)
     3.8  
     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Apr 13 13:59:35 2012 +0200
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Apr 13 14:00:26 2012 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Library/Quotient3_Set.thy
     4.5 +(*  Title:      HOL/Library/Quotient_Set.thy
     4.6      Author:     Cezary Kaliszyk and Christian Urban
     4.7  *)
     4.8  
     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 13 13:59:35 2012 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 13 14:00:26 2012 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/Library/Quotient3_Sum.thy
     5.5 +(*  Title:      HOL/Library/Quotient_Sum.thy
     5.6      Author:     Cezary Kaliszyk and Christian Urban
     5.7  *)
     5.8  
     6.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Apr 13 13:59:35 2012 +0200
     6.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Apr 13 14:00:26 2012 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      RBT_Impl.thy
     6.5 +(*  Title:      HOL/Library/RBT_Impl.thy
     6.6      Author:     Markus Reiter, TU Muenchen
     6.7      Author:     Alexander Krauss, TU Muenchen
     6.8  *)
     7.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Apr 13 13:59:35 2012 +0200
     7.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Apr 13 14:00:26 2012 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/Matrix/ComputeFloat.thy
     7.5 +(*  Title:      HOL/Matrix_LP/ComputeFloat.thy
     7.6      Author:     Steven Obua
     7.7  *)
     7.8  
     8.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Apr 13 13:59:35 2012 +0200
     8.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Apr 13 14:00:26 2012 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Matrix/Compute_Oracle/Compute_Oracle.thy
     8.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
     8.6      Author:     Steven Obua, TU Munich
     8.7  
     8.8  Steven Obua's evaluator.
     9.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Fri Apr 13 13:59:35 2012 +0200
     9.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Fri Apr 13 14:00:26 2012 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Matrix/Compute_Oracle/am_compiler.ML
     9.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
     9.6      Author:     Steven Obua
     9.7  *)
     9.8  
    10.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Fri Apr 13 13:59:35 2012 +0200
    10.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML	Fri Apr 13 14:00:26 2012 +0200
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      HOL/Matrix/Compute_Oracle/am_ghc.ML
    10.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_ghc.ML
    10.6      Author:     Steven Obua
    10.7  *)
    10.8  
    11.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML	Fri Apr 13 13:59:35 2012 +0200
    11.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML	Fri Apr 13 14:00:26 2012 +0200
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      HOL/Matrix/Compute_Oracle/am_interpreter.ML
    11.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML
    11.6      Author:     Steven Obua
    11.7  *)
    11.8  
    12.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Fri Apr 13 13:59:35 2012 +0200
    12.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Fri Apr 13 14:00:26 2012 +0200
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      HOL/Matrix/Compute_Oracle/am_sml.ML
    12.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/am_sml.ML
    12.6      Author:     Steven Obua
    12.7  
    12.8  TODO: "parameterless rewrite cannot be used in pattern": In a lot of
    13.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Apr 13 13:59:35 2012 +0200
    13.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Fri Apr 13 14:00:26 2012 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/Matrix/Compute_Oracle/compute.ML
    13.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/compute.ML
    13.6      Author:     Steven Obua
    13.7  *)
    13.8  
    14.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Apr 13 13:59:35 2012 +0200
    14.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Apr 13 14:00:26 2012 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOL/Matrix/Compute_Oracle/linker.ML
    14.5 +(*  Title:      HOL/Matrix_LP/Compute_Oracle/linker.ML
    14.6      Author:     Steven Obua
    14.7  
    14.8  This module solves the problem that the computing oracle does not
    15.1 --- a/src/HOL/Matrix_LP/Cplex.thy	Fri Apr 13 13:59:35 2012 +0200
    15.2 +++ b/src/HOL/Matrix_LP/Cplex.thy	Fri Apr 13 14:00:26 2012 +0200
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      HOL/Matrix/Cplex.thy
    15.5 +(*  Title:      HOL/Matrix_LP/Cplex.thy
    15.6      Author:     Steven Obua
    15.7  *)
    15.8  
    16.1 --- a/src/HOL/Matrix_LP/CplexMatrixConverter.ML	Fri Apr 13 13:59:35 2012 +0200
    16.2 +++ b/src/HOL/Matrix_LP/CplexMatrixConverter.ML	Fri Apr 13 14:00:26 2012 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOL/Matrix/CplexMatrixConverter.ML
    16.5 +(*  Title:      HOL/Matrix_LP/CplexMatrixConverter.ML
    16.6      Author:     Steven Obua
    16.7  *)
    16.8  
    17.1 --- a/src/HOL/Matrix_LP/Cplex_tools.ML	Fri Apr 13 13:59:35 2012 +0200
    17.2 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Fri Apr 13 14:00:26 2012 +0200
    17.3 @@ -1,4 +1,4 @@
    17.4 -(*  Title:      HOL/Matrix/Cplex_tools.ML
    17.5 +(*  Title:      HOL/Matrix_LP/Cplex_tools.ML
    17.6      Author:     Steven Obua
    17.7  *)
    17.8  
    18.1 --- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri Apr 13 13:59:35 2012 +0200
    18.2 +++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri Apr 13 14:00:26 2012 +0200
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/Matrix/FloatSparseMatrixBuilder.ML
    18.5 +(*  Title:      HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
    18.6      Author:     Steven Obua
    18.7  *)
    18.8  
    19.1 --- a/src/HOL/Matrix_LP/LP.thy	Fri Apr 13 13:59:35 2012 +0200
    19.2 +++ b/src/HOL/Matrix_LP/LP.thy	Fri Apr 13 14:00:26 2012 +0200
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title:      HOL/Matrix/LP.thy
    19.5 +(*  Title:      HOL/Matrix_LP/LP.thy
    19.6      Author:     Steven Obua
    19.7  *)
    19.8  
    20.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Fri Apr 13 13:59:35 2012 +0200
    20.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Apr 13 14:00:26 2012 +0200
    20.3 @@ -1,4 +1,4 @@
    20.4 -(*  Title:      HOL/Matrix/Matrix.thy
    20.5 +(*  Title:      HOL/Matrix_LP/Matrix.thy
    20.6      Author:     Steven Obua
    20.7  *)
    20.8  
    21.1 --- a/src/HOL/Matrix_LP/SparseMatrix.thy	Fri Apr 13 13:59:35 2012 +0200
    21.2 +++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Fri Apr 13 14:00:26 2012 +0200
    21.3 @@ -1,4 +1,4 @@
    21.4 -(*  Title:      HOL/Matrix/SparseMatrix.thy
    21.5 +(*  Title:      HOL/Matrix_LP/SparseMatrix.thy
    21.6      Author:     Steven Obua
    21.7  *)
    21.8  
    22.1 --- a/src/HOL/Matrix_LP/fspmlp.ML	Fri Apr 13 13:59:35 2012 +0200
    22.2 +++ b/src/HOL/Matrix_LP/fspmlp.ML	Fri Apr 13 14:00:26 2012 +0200
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      HOL/Matrix/fspmlp.ML
    22.5 +(*  Title:      HOL/Matrix_LP/fspmlp.ML
    22.6      Author:     Steven Obua
    22.7  *)
    22.8  
    23.1 --- a/src/HOL/Matrix_LP/matrixlp.ML	Fri Apr 13 13:59:35 2012 +0200
    23.2 +++ b/src/HOL/Matrix_LP/matrixlp.ML	Fri Apr 13 14:00:26 2012 +0200
    23.3 @@ -1,4 +1,4 @@
    23.4 -(*  Title:      HOL/Matrix/matrixlp.ML
    23.5 +(*  Title:      HOL/Matrix_LP/matrixlp.ML
    23.6      Author:     Steven Obua
    23.7  *)
    23.8  
    24.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Fri Apr 13 13:59:35 2012 +0200
    24.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Apr 13 14:00:26 2012 +0200
    24.3 @@ -1,4 +1,4 @@
    24.4 -(*  Title:      HOL/Quotient3_Examples/FSet.thy
    24.5 +(*  Title:      HOL/Quotient_Examples/FSet.thy
    24.6      Author:     Cezary Kaliszyk, TU Munich
    24.7      Author:     Christian Urban, TU Munich
    24.8  
    25.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Apr 13 13:59:35 2012 +0200
    25.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Apr 13 14:00:26 2012 +0200
    25.3 @@ -1,4 +1,4 @@
    25.4 -(*  Title:      HOL/Quotient3_Examples/Lift_Fun.thy
    25.5 +(*  Title:      HOL/Quotient_Examples/Lift_Fun.thy
    25.6      Author:     Ondrej Kuncar
    25.7  *)
    25.8  
    26.1 --- a/src/HOL/Tools/legacy_transfer.ML	Fri Apr 13 13:59:35 2012 +0200
    26.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Fri Apr 13 14:00:26 2012 +0200
    26.3 @@ -1,7 +1,7 @@
    26.4 -(*  Title:      HOL/Tools/transfer.ML
    26.5 +(*  Title:      HOL/Tools/legacy_transfer.ML
    26.6      Author:     Amine Chaieb, University of Cambridge, 2009
    26.7 -                Jeremy Avigad, Carnegie Mellon University
    26.8 -                Florian Haftmann, TU Muenchen
    26.9 +    Author:     Jeremy Avigad, Carnegie Mellon University
   26.10 +    Author:     Florian Haftmann, TU Muenchen
   26.11  
   26.12  Simple transfer principle on theorems.
   26.13  *)