--- 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
*)