Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated headers;
authorwenzelm
Fri, 13 Apr 2012 14:00:26 +0200
changeset 47455 26315a545e26
parent 47454 479b4d6b9562
child 47456 88adecfe4246
updated headers;
src/HOL/Library/Quotient_List.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Option.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Product.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Set.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Quotient_Sum.thy file | annotate | diff | comparison | revisions
src/HOL/Library/RBT_Impl.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/ComputeFloat.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/am_interpreter.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/compute.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Compute_Oracle/linker.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Cplex.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/CplexMatrixConverter.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Cplex_tools.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/LP.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/Matrix.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/SparseMatrix.thy file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/fspmlp.ML file | annotate | diff | comparison | revisions
src/HOL/Matrix_LP/matrixlp.ML file | annotate | diff | comparison | revisions
src/HOL/Quotient_Examples/FSet.thy file | annotate | diff | comparison | revisions
src/HOL/Quotient_Examples/Lift_Fun.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/legacy_transfer.ML file | annotate | diff | comparison | revisions 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
--- 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
 *)
 
--- 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.
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
--- 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
 *)
 
--- 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
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 *)
 
--- 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
 
--- 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
 *)
 
--- 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.
 *)
isabelle