author haftmann Mon, 23 Mar 2009 08:14:23 +0100 changeset 30661 54858c8ad226 parent 30660 53e1b1641f09 child 30662 396be15b95d5
 src/HOL/Library/Determinants.thy file | annotate | diff | comparison | revisions src/HOL/Library/Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Library/Finite_Cartesian_Product.thy file | annotate | diff | comparison | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions src/HOL/Library/Glbs.thy file | annotate | diff | comparison | revisions src/HOL/Library/Order_Relation.thy file | annotate | diff | comparison | revisions src/HOL/ex/MergeSort.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Library/Determinants.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Determinants.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -5,7 +5,7 @@
header {* Traces, Determinant of square matrices and some properties *}

theory Determinants
-  imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations
begin

subsection{* First some facts about products*}```
```--- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -5,10 +5,10 @@
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}

theory Euclidean_Space
-  imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
-  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
-  Inner_Product
-  uses ("normarith.ML")
+imports
+  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product
+uses ("normarith.ML")
begin

text{* Some common special cases.*}```
```--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -5,12 +5,9 @@
header {* Definition of finite Cartesian product types. *}

theory Finite_Cartesian_Product
-  (* imports Plain SetInterval ATP_Linkup *)
-imports Main
+imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
begin

-  (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*)
-
definition hassize (infixr "hassize" 12) where
"(S hassize n) = (finite S \<and> card S = n)"
```
```--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      Formal_Power_Series.thy
-    ID:
Author:     Amine Chaieb, University of Cambridge
*)

header{* A formalization of formal power series *}

theory Formal_Power_Series
-  imports Main Fact Parity
+imports Main Fact Parity
begin

subsection {* The type of formal power series*}```
```--- a/src/HOL/Library/Glbs.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Glbs.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,8 +1,6 @@
-(* Title:      Glbs
-   Author:     Amine Chaieb, University of Cambridge
-*)
+(* Author: Amine Chaieb, University of Cambridge *)

-header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*}
+header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}

theory Glbs
imports Lubs```
```--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,6 +1,4 @@
-(*  ID          : \$Id\$
-    Author      : Tobias Nipkow
-*)
+(* Author: Tobias Nipkow *)

header {* Orders as Relations *}
```
```--- a/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:14:22 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:14:23 2009 +0100
@@ -1,5 +1,4 @@
(*  Title:      HOL/ex/Merge.thy
-    ID:         \$Id\$
Author:     Tobias Nipkow
Copyright   2002 TU Muenchen
*)```