# HG changeset patch # User wenzelm # Date 1236207167 -3600 # Node ID 171b3bd93c905aa65bf63e558e1ef0e2954bde0c # Parent 970bf4f594c94ede73a5f9930c7e7c8c07e7f83e removed old/broken CVS Ids; diff -r 970bf4f594c9 -r 171b3bd93c90 src/HOL/Library/Determinants.thy --- a/src/HOL/Library/Determinants.thy Wed Mar 04 23:05:32 2009 +0100 +++ b/src/HOL/Library/Determinants.thy Wed Mar 04 23:52:47 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Determinants - ID: $Id: Author: Amine Chaieb, University of Cambridge *) diff -r 970bf4f594c9 -r 171b3bd93c90 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Wed Mar 04 23:05:32 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Wed Mar 04 23:52:47 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Library/Euclidean_Space - ID: $Id: Author: Amine Chaieb, University of Cambridge *) diff -r 970bf4f594c9 -r 171b3bd93c90 src/HOL/Library/Finite_Cartesian_Product.thy --- a/src/HOL/Library/Finite_Cartesian_Product.thy Wed Mar 04 23:05:32 2009 +0100 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy Wed Mar 04 23:52:47 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/Finite_Cartesian_Product - ID: $Id: Finite_Cartesian_Product.thy,v 1.5 2009/01/29 22:59:46 chaieb Exp $ Author: Amine Chaieb, University of Cambridge *) diff -r 970bf4f594c9 -r 171b3bd93c90 src/HOL/Library/Glbs.thy --- a/src/HOL/Library/Glbs.thy Wed Mar 04 23:05:32 2009 +0100 +++ b/src/HOL/Library/Glbs.thy Wed Mar 04 23:52:47 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Glbs - ID: $Id: Author: Amine Chaieb, University of Cambridge *) diff -r 970bf4f594c9 -r 171b3bd93c90 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Wed Mar 04 23:05:32 2009 +0100 +++ b/src/HOL/Library/Permutations.thy Wed Mar 04 23:52:47 2009 +0100 @@ -1,5 +1,4 @@ (* Title: Library/Permutations - ID: $Id: Author: Amine Chaieb, University of Cambridge *) diff -r 970bf4f594c9 -r 171b3bd93c90 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Mar 04 23:05:32 2009 +0100 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Wed Mar 04 23:52:47 2009 +0100 @@ -1,7 +1,7 @@ (* Title: Topology - ID: $Id: Author: Amine Chaieb, University of Cambridge - Robert Himmelmann, TU Muenchen*) + Author: Robert Himmelmann, TU Muenchen +*) header {* Elementary topology in Euclidean space. *}