author haftmann Mon, 23 Mar 2009 08:16:24 +0100 changeset 30665 4cf38ea4fad2 parent 30659 a400b06d03cb (current diff) parent 30664 167da873c3b3 (diff) child 30666 d6248d4508d5 child 30684 c98a64746c69 child 30734 ab05be086c4a
merged
--- a/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,11 +1,14 @@
(*  Title:      HOL/Import/HOL4Compat.thy
-    ID:         $Id$
Author:     Sebastian Skalberg (TU Muenchen)
*)

-theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
+theory HOL4Compat
+imports HOL4Setup Complex_Main Primes ContNotDenum
begin

+no_notation differentiable (infixl "differentiable" 60)
+no_notation sums (infixr "sums" 80)
+
lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
by auto

@@ -22,7 +25,7 @@
lemmas [hol4rew] = ONE_ONE_rew

lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
-  by simp;
+  by simp

lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
by safe
--- a/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Abstract_Rat.thy
-    ID:         $Id$
Author:     Amine Chaieb
*)

header {* Abstract rational numbers *}

theory Abstract_Rat
-imports Plain GCD
+imports GCD Main
begin

types Num = "int \<times> int"
--- a/src/HOL/Library/AssocList.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/AssocList.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/AssocList.thy
-    ID:         $Id$
Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
*)

header {* Map operations implemented on association lists*}

theory AssocList
-imports Plain "~~/src/HOL/Map"
+imports Map Main
begin

text {*
--- a/src/HOL/Library/Binomial.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -6,7 +6,7 @@
header {* Binomial Coefficients *}

theory Binomial
-imports Fact Plain "~~/src/HOL/SetInterval" Presburger
+imports Fact SetInterval Presburger Main
begin

text {* This development is based on the work of Andy Gordon and
--- a/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Boolean Algebras *}

theory Boolean_Algebra
-imports Plain
+imports Main
begin

locale boolean =
--- a/src/HOL/Library/Char_nat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Char_nat.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Char_nat.thy
-    ID:         $Id$
Author:     Norbert Voelker, Florian Haftmann
*)

header {* Mapping between characters and natural numbers *}

theory Char_nat
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

text {* Conversions between nibbles and natural numbers in [0..15]. *}
--- a/src/HOL/Library/Char_ord.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Char_ord.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Char_ord.thy
-    ID:         $Id$
Author:     Norbert Voelker, Florian Haftmann
*)

header {* Order on characters *}

theory Char_ord
-imports Plain Product_ord Char_nat
+imports Product_ord Char_nat Main
begin

instantiation nibble :: linorder
--- a/src/HOL/Library/Code_Char.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Code generation of pretty characters (and strings) *}

theory Code_Char
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
+imports List Code_Eval Main
begin

code_type char
--- a/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Code_Char_chr.thy
-    ID:         $Id$
Author:     Florian Haftmann
*)

header {* Code generation of pretty characters with character codes *}

theory Code_Char_chr
-imports Plain Char_nat Code_Char Code_Integer
+imports Char_nat Code_Char Code_Integer Main
begin

definition
--- a/src/HOL/Library/Code_Index.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Index.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -3,7 +3,7 @@
header {* Type of indices *}

theory Code_Index
-imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
+imports Main
begin

text {*
--- a/src/HOL/Library/Code_Integer.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Pretty integer literals for code generation *}

theory Code_Integer
-imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
+imports Main
begin

text {*
--- a/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Coinductive_Lists.thy
-    ID:         $Id$
Author:     Lawrence C Paulson and Makarius
*)

header {* Potentially infinite lists as greatest fixed-point *}

theory Coinductive_List
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

subsection {* List constructors over the datatype universe *}
--- a/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -6,7 +6,7 @@
header {* Proving equalities in commutative rings *}

theory Commutative_Ring
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Parity"
+imports List Parity Main
uses ("comm_ring.ML")
begin

--- a/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Non-denumerability of the Continuum. *}

theory ContNotDenum
-imports RComplete Hilbert_Choice
+imports Complex_Main
begin

subsection {* Abstract *}
--- a/src/HOL/Library/Continuity.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Continuity.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Continuity.thy
-    ID:         $Id$
Author:     David von Oheimb, TU Muenchen
*)

header {* Continuity and iterations (of set transformers) *}

theory Continuity
-imports Plain "~~/src/HOL/Relation_Power"
+imports Relation_Power Main
begin

subsection {* Continuity for complete lattices *}
--- a/src/HOL/Library/Countable.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -6,11 +6,11 @@

theory Countable
imports
-  Plain
"~~/src/HOL/List"
"~~/src/HOL/Hilbert_Choice"
"~~/src/HOL/Nat_Int_Bij"
"~~/src/HOL/Rational"
+  Main
begin

subsection {* The class of countable types *}
--- a/src/HOL/Library/Determinants.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Determinants.thy	Mon Mar 23 08:16:24 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/Efficient_Nat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Implementation of natural numbers by target-language integers *}

theory Efficient_Nat
-imports Code_Index Code_Integer
+imports Code_Index Code_Integer Main
begin

text {*
--- a/src/HOL/Library/Enum.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Enum.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Finite types as explicit enumerations *}

theory Enum
-imports Plain "~~/src/HOL/Map"
+imports Map Main
begin

subsection {* Class @{text enum} *}
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,8 @@
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}

theory Euclidean_Space
-imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports
+  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
Inner_Product
uses ("normarith.ML")
--- a/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Evaluation Oracle with ML witnesses *}

theory Eval_Witness
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

text {* 
--- a/src/HOL/Library/Executable_Set.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Executable_Set.thy
-    ID:         $Id$
Author:     Stefan Berghofer, TU Muenchen
*)

header {* Implementation of finite sets by lists *}

theory Executable_Set
-imports Plain "~~/src/HOL/List"
+imports Main
begin

subsection {* Definitional rewrites *}
--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:16:24 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 07:41:07 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:16:24 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/FrechetDeriv.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title       : FrechetDeriv.thy
-    ID          : $Id$
Author      : Brian Huffman
*)

header {* Frechet Derivative *}

theory FrechetDeriv
-imports Lim
+imports Lim Complex_Main
begin

definition
--- a/src/HOL/Library/FuncSet.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/FuncSet.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/FuncSet.thy
-    ID:         $Id$
Author:     Florian Kammueller and Lawrence C Paulson
*)

header {* Pi and Function Sets *}

theory FuncSet
-imports Plain "~~/src/HOL/Hilbert_Choice"
+imports Hilbert_Choice Main
begin

definition
--- a/src/HOL/Library/Glbs.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Glbs.thy	Mon Mar 23 08:16:24 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/Infinite_Set.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,15 +1,13 @@
(*  Title:      HOL/Library/Infinite_Set.thy
-    ID:         $Id$
Author:     Stephan Merz
*)

header {* Infinite Sets and Related Concepts *}

theory Infinite_Set
-imports Main "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
+imports Main
begin

-
subsection "Infinite Sets"

text {*
--- a/src/HOL/Library/Inner_Product.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Inner Product Spaces and the Gradient Derivative *}

theory Inner_Product
-imports Complex FrechetDeriv
+imports Complex_Main FrechetDeriv
begin

subsection {* Real inner product spaces *}
--- a/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@

(*<*)
theory LaTeXsugar
-imports Plain "~~/src/HOL/List"
+imports Main
begin

(* LOGIC *)
--- a/src/HOL/Library/ListVector.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/ListVector.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,11 +1,9 @@
-(*  ID:         $Id$
-    Author:     Tobias Nipkow, 2007
-*)
+(*  Author: Tobias Nipkow, 2007 *)

-header "Lists as vectors"
+header {* Lists as vectors *}

theory ListVector
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

text{* \noindent
--- a/src/HOL/Library/List_Prefix.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/List_Prefix.thy
-    ID:         $Id$
Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
*)

header {* List prefixes and postfixes *}

theory List_Prefix
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

subsection {* Prefix order on lists *}
--- a/src/HOL/Library/List_lexord.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/List_lexord.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/List_lexord.thy
-    ID:         $Id$
Author:     Norbert Voelker
*)

header {* Lexicographic order on lists *}

theory List_lexord
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

instantiation list :: (ord) ord
--- a/src/HOL/Library/Mapping.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* An abstract view on maps for code generation. *}

theory Mapping
-imports Map
+imports Map Main
begin

subsection {* Type definition and primitive operations *}
--- a/src/HOL/Library/Multiset.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Multisets *}

theory Multiset
-imports Plain "~~/src/HOL/List"
+imports List Main
begin

subsection {* The type of multisets *}
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Natural numbers with infinity *}

theory Nat_Infinity
-imports Plain "~~/src/HOL/Presburger"
+imports Main
begin

subsection {* Type definition *}
--- a/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Nat_Int_Bij.thy
-    ID:         $Id$
Author:     Stefan Richter, Tobias Nipkow
*)

header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}

theory Nat_Int_Bij
-imports Hilbert_Choice Presburger
+imports Main
begin

subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
--- a/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
(*  Title:      HOL/Library/Nested_Environment.thy
-    ID:         $Id$
Author:     Markus Wenzel, TU Muenchen
*)

header {* Nested environments *}

theory Nested_Environment
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
+imports Main
begin

text {*
--- a/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Numeral Syntax for Types *}

theory Numeral_Type
-imports Plain "~~/src/HOL/Presburger"
+imports Main
begin

subsection {* Preliminary lemmas *}
--- a/src/HOL/Library/Option_ord.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,15 +1,14 @@
(*  Title:      HOL/Library/Option_ord.thy
-    ID:         $Id$
Author:     Florian Haftmann, TU Muenchen
*)

header {* Canonical order on option type *}

theory Option_ord
-imports Plain
+imports Option Main
begin

-instantiation option :: (order) order
+instantiation option :: (preorder) preorder
begin

definition less_eq_option where
@@ -48,12 +47,63 @@
lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
by (simp add: less_option_def)

-instance by default
-  (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance proof
+qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)

end

-instance option :: (linorder) linorder
-  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance option :: (order) order proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instance option :: (linorder) linorder proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instantiation option :: (preorder) bot
+begin
+
+definition "bot = None"
+
+instance proof
+qed (simp add: bot_option_def)
+
+end
+
+instantiation option :: (top) top
+begin
+
+definition "top = Some top"
+
+instance proof
+qed (simp add: top_option_def less_eq_option_def split: option.split)

end
+
+instance option :: (wellorder) wellorder proof
+  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
+  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  have "P None" by (rule H) simp
+  then have P_Some [case_names Some]:
+    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
+  proof -
+    fix z
+    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
+    with P None show "P z" by (cases z) simp_all
+  qed
+  show "P z" proof (cases z rule: P_Some)
+    case (Some w)
+    show "(P o Some) w" proof (induct rule: less_induct)
+      case (less x)
+      have "P (Some x)" proof (rule H)
+        fix y :: "'a option"
+        assume "y < Some x"
+        show "P y" proof (cases y rule: P_Some)
+          case (Some v) with y < Some x have "v < x" by simp
+          with less show "(P o Some) v" .
+        qed
+      qed
+      then show ?case by simp
+    qed
+  qed
+qed
+
+end
--- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -4,7 +4,7 @@
*)
(*<*)
theory OptionalSugar
-imports LaTeXsugar Complex_Main
+imports Complex_Main LaTeXsugar
begin

(* hiding set *)
--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,6 +1,4 @@
-(*  ID          : $Id$
-    Author      : Tobias Nipkow
-*)
+(* Author: Tobias Nipkow *)

header {* Orders as Relations *}

--- a/src/HOL/Library/Permutations.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Permutations.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Permutations, both general and specifically on finite sets.*}

theory Permutations
-imports Main Finite_Cartesian_Product Parity Fact
+imports Finite_Cartesian_Product Parity Fact Main
begin

(* Why should I import Main just to solve the Typerep problem! *)
--- a/src/HOL/Library/Zorn.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Zorn.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -7,7 +7,7 @@
header {* Zorn's Lemma *}

theory Zorn
-imports "~~/src/HOL/Order_Relation"
+imports Order_Relation Main
begin

(* Define globally? In Set.thy? *)
--- a/src/HOL/ex/MergeSort.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
(*  Title:      HOL/ex/Merge.thy
-    ID:         $Id$
Author:     Tobias Nipkow
Copyright   2002 TU Muenchen
*)