# HG changeset patch
# User nipkow
# Date 1092820180 -7200
# Node ID 322485b816ac88054c4505e1ebee0c72152e09d6
# Parent  58cd3404cf75743b45cb668a3b21c47c52ff7987
import -> imports

diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/CLim.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Limits, Continuity and Differentiation for Complex Functions*}
 
 theory CLim
-import CSeries
+imports CSeries
 begin
 
 (*not in simpset?*)
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/CSeries.thy
--- a/src/HOL/Complex/CSeries.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/CSeries.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header{*Finite Summation and Infinite Series for Complex Numbers*}
 
 theory CSeries
-import CStar
+imports CStar
 begin
 
 consts sumc :: "[nat,nat,(nat=>complex)] => complex"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/CStar.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
       and Complex Functions*}
 
 theory CStar
-import NSCA
+imports NSCA
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header {* Complex Numbers: Rectangular and Polar Representations *}
 
 theory Complex
-import "../Hyperreal/HLog"
+imports "../Hyperreal/HLog"
 begin
 
 datatype complex = Complex real real
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/ComplexBin.thy
--- a/src/HOL/Complex/ComplexBin.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/ComplexBin.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory ComplexBin
-import Complex
+imports Complex
 begin
 
 end
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/Complex_Main.thy
--- a/src/HOL/Complex/Complex_Main.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/Complex_Main.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Comprehensive Complex Theory*}
 
 theory Complex_Main
-import CLim
+imports CLim
 begin
 
 end
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/NSCA.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header{*Non-Standard Complex Analysis*}
 
 theory NSCA
-import NSComplex
+imports NSComplex
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Nonstandard Complex Numbers*}
 
 theory NSComplex
-import Complex
+imports Complex
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Datatype.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Datatypes *}
 
 theory Datatype
-import Datatype_Universe
+imports Datatype_Universe
 begin
 
 subsection {* Representing primitive types *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Divides.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Divides
-import NatArith
+imports NatArith
 begin
 
 (*We use the same class for div and mod;
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Extraction.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Program extraction for HOL *}
 
 theory Extraction
-import Datatype
+imports Datatype
 files "Tools/rewrite_hol_proof.ML"
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-import Divides Power Inductive
+imports Divides Power Inductive
 begin
 
 subsection {* Collection of finite sets *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Fun.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Fun 
-import Typedef
+imports Typedef
 begin
 
 instance set :: (type) order
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Gfp.thy
--- a/src/HOL/Gfp.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Gfp.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Gfp 
-import Lfp
+imports Lfp
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* The basis of Higher-Order Logic *}
 
 theory HOL
-import CPure
+imports CPure
 files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-import NatArith
+imports NatArith
 files ("Tools/meson.ML") ("Tools/specification_package.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/EvenOdd.thy
--- a/src/HOL/Hyperreal/EvenOdd.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Even and Odd Numbers: Compatibility file for Parity*}
 
 theory EvenOdd
-import NthRoot
+imports NthRoot
 begin
 
 subsection{*General Lemmas About Division*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Fact.thy
--- a/src/HOL/Hyperreal/Fact.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Factorial Function*}
 
 theory Fact
-import Real
+imports Real
 begin
 
 consts fact :: "nat => nat"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Filter.thy
--- a/src/HOL/Hyperreal/Filter.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Filter.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Filters and Ultrafilters*}
 
 theory Filter
-import Zorn
+imports Zorn
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header{*Logarithms: Non-Standard Version*}
 
 theory HLog
-import Log HTranscendental
+imports Log HTranscendental
 begin
 
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Finite Summation and Infinite Series for Hyperreals*}
 
 theory HSeries
-import Series
+imports Series
 begin
 
 constdefs 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Nonstandard Extensions of Transcendental Functions*}
 
 theory HTranscendental
-import Transcendental Integration
+imports Transcendental Integration
 begin
 
 text{*really belongs in Transcendental*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Binary arithmetic and Simplification for the Hyperreals*}
 
 theory HyperArith
-import HyperDef
+imports HyperDef
 files ("hypreal_arith.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
-import Filter "../Real/Real"
+imports Filter "../Real/Real"
 files ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Construction of Hypernaturals using Ultrafilters*}
 
 theory HyperNat
-import Star
+imports Star
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Exponentials on the Hyperreals*}
 
 theory HyperPow
-import HyperArith HyperNat "../Real/RealPow"
+imports HyperArith HyperNat "../Real/RealPow"
 begin
 
 instance hypreal :: power ..
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Hyperreal.thy
--- a/src/HOL/Hyperreal/Hyperreal.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Hyperreal.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 *)
 
 theory Hyperreal
-import Poly MacLaurin HLog
+imports Poly MacLaurin HLog
 begin
 
 end
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Theory of Integration*}
 
 theory Integration
-import MacLaurin
+imports MacLaurin
 begin
 
 text{*We follow John Harrison in formalizing the Gauge integral.*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Limits, Continuity and Differentiation*}
 
 theory Lim
-import SEQ RealDef
+imports SEQ RealDef
 begin
 
 text{*Standard and Nonstandard Definitions*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Log.thy
--- a/src/HOL/Hyperreal/Log.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Log.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header{*Logarithms: Standard Version*}
 
 theory Log
-import Transcendental
+imports Transcendental
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory MacLaurin
-import Log
+imports Log
 begin
 
 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
 theory NSA
-import HyperArith RComplete
+imports HyperArith RComplete
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Star-transforms for the Hypernaturals*}
 
 theory NatStar
-import "../Real/RealPow" HyperPow
+imports "../Real/RealPow" HyperPow
 begin
 
 text{*Extends sets of nats, and functions from the nats to nats or reals*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Existence of Nth Root*}
 
 theory NthRoot
-import SEQ HSeries
+imports SEQ HSeries
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header{*Univariate Real Polynomials*}
 
 theory Poly
-import Transcendental
+imports Transcendental
 begin
 
 text{*Application of polynomial as a real function.*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory SEQ
-import NatStar HyperPow
+imports NatStar HyperPow
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Finite Summation and Infinite Series*}
 
 theory Series
-import SEQ Lim
+imports SEQ Lim
 begin
 
 syntax sumr :: "[nat,nat,(nat=>real)] => real"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Star-Transforms in Non-Standard Analysis*}
 
 theory Star
-import NSA
+imports NSA
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Power Series, Transcendental Functions etc.*}
 
 theory Transcendental
-import NthRoot Fact HSeries EvenOdd Lim
+imports NthRoot Fact HSeries EvenOdd Lim
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Inductive.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Support for inductive sets and types *}
 
 theory Inductive 
-import Gfp Sum_Type Relation Record
+imports Gfp Sum_Type Relation Record
 files
   ("Tools/inductive_package.ML")
   ("Tools/inductive_realizer.ML")
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Infnite Sets and Related Concepts*}
 
 theory Infinite_Set
-import Hilbert_Choice Finite_Set SetInterval
+imports Hilbert_Choice Finite_Set SetInterval
 begin
 
 subsection "Infinite Sets"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/Equiv.thy
--- a/src/HOL/Integ/Equiv.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Equivalence relations in Higher-Order Set Theory *}
 
 theory Equiv
-import Relation Finite_Set
+imports Relation Finite_Set
 begin
 
 subsection {* Equivalence relations *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/IntArith.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Integer arithmetic *}
 
 theory IntArith
-import Numeral
+imports Numeral
 files ("int_arith1.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
 
 theory IntDef
-import Equiv NatArith
+imports Equiv NatArith
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -32,7 +32,7 @@
 
 
 theory IntDiv
-import IntArith Recdef
+imports IntArith Recdef
 files ("IntDiv_setup.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Binary arithmetic for the natural numbers *}
 
 theory NatBin
-import IntDiv
+imports IntDiv
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {*Simprocs for the Naturals*}
 
 theory NatSimprocs
-import NatBin
+imports NatBin
 files "int_factor_simprocs.ML" "nat_simprocs.ML"
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/Numeral.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Arithmetic on Binary Integers*}
 
 theory Numeral
-import IntDef
+imports IntDef
 files "Tools/numeral_syntax.ML"
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/Parity.thy
--- a/src/HOL/Integ/Parity.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/Parity.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Parity: Even and Odd for ints and nats*}
 
 theory Parity
-import Divides IntDiv NatSimprocs
+imports Divides IntDiv NatSimprocs
 begin
 
 axclass even_odd < type
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header {* Presburger Arithmetic: Cooper's Algorithm *}
 
 theory Presburger
-import NatSimprocs SetInterval
+imports NatSimprocs SetInterval
 files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/LOrder.thy
--- a/src/HOL/LOrder.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/LOrder.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Lattice Orders *}
 
 theory LOrder
-import HOL
+imports HOL
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Lfp.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Lfp
-import Product_Type
+imports Product_Type
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Accessible_Part.thy
--- a/src/HOL/Library/Accessible_Part.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Accessible_Part.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* The accessible part of a relation *}
 
 theory Accessible_Part
-import Main
+imports Main
 begin
 
 subsection {* Inductive definition *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Continuity.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Continuity and iterations (of set transformers) *}
 
 theory Continuity
-import Main
+imports Main
 begin
 
 subsection "Chains"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Pi and Function Sets *}
 
 theory FuncSet
-import Main
+imports Main
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Library.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Library
-import
+imports
   Accessible_Part
   Continuity
   FuncSet
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* List prefixes and postfixes *}
 
 theory List_Prefix
-import Main
+imports Main
 begin
 
 subsection {* Prefix order on lists *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Multisets *}
 
 theory Multiset
-import Accessible_Part
+imports Accessible_Part
 begin
 
 subsection {* The type of multisets *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/NatPair.thy
--- a/src/HOL/Library/NatPair.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/NatPair.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Pairs of Natural Numbers *}
 
 theory NatPair
-import Main
+imports Main
 begin
 
 text{*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Natural numbers with infinity *}
 
 theory Nat_Infinity
-import Main
+imports Main
 begin
 
 subsection "Definitions"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Nested environments *}
 
 theory Nested_Environment
-import Main
+imports Main
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Permutation.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -5,7 +5,7 @@
 header {* Permutations *}
 
 theory Permutation
-import Multiset
+imports Multiset
 begin
 
 consts
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Primes.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* The Greatest Common Divisor and Euclid's algorithm *}
 
 theory Primes
-import Main
+imports Main
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Quotient.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Quotient types *}
 
 theory Quotient
-import Main
+imports Main
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* A general ``while'' combinator *}
 
 theory While_Combinator
-import Main
+imports Main
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Word.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Binary Words *}
 
 theory Word
-import Main
+imports Main
 files "word_setup.ML"
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Library/Zorn.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Zorn's Lemma *}
 
 theory Zorn
-import Main
+imports Main
 begin
 
 text{*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/List.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-import PreList
+imports PreList
 begin
 
 datatype 'a list =
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Main.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Main HOL *}
 
 theory Main
-import Map Infinite_Set Extraction Refute
+imports Map Infinite_Set Extraction Refute
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Map.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header {* Maps *}
 
 theory Map
-import List
+imports List
 begin
 
 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Nat.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header {* Natural numbers *}
 
 theory Nat
-import Wellfounded_Recursion Ring_and_Field
+imports Wellfounded_Recursion Ring_and_Field
 begin
 
 subsection {* Type @{text ind} *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/NatArith.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* More arithmetic on natural numbers *}
 
 theory NatArith
-import Nat
+imports Nat
 files "arith_data.ML"
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Ordered Groups *}
 
 theory OrderedGroup
-import Inductive LOrder
+imports Inductive LOrder
 files "../Provers/Arith/abel_cancel.ML"
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Power.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Exponentiation and Binomial Coefficients*}
 
 theory Power
-import Divides
+imports Divides
 begin
 
 subsection{*Powers for Arbitrary Semirings*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/PreList.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*A Basis for Building the Theory of Lists*}
 
 theory PreList
-import Wellfounded_Relations Presburger Recdef Relation_Power Parity
+imports Wellfounded_Relations Presburger Recdef Relation_Power Parity
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Presburger.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header {* Presburger Arithmetic: Cooper's Algorithm *}
 
 theory Presburger
-import NatSimprocs SetInterval
+imports NatSimprocs SetInterval
 files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Cartesian products *}
 
 theory Product_Type
-import Fun
+imports Fun
 files ("Tools/split_rule.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Real/Lubs.thy
--- a/src/HOL/Real/Lubs.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/Lubs.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header{*Definitions of Upper Bounds and Least Upper Bounds*}
 
 theory Lubs
-import Main
+imports Main
 begin
 
 text{*Thanks to suggestions by James Margetson*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 *)
 
 theory PReal
-import Rational
+imports Rational
 begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/RComplete.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header{*Completeness of the Reals; Floor and Ceiling Functions*}
 
 theory RComplete
-import Lubs RealDef
+imports Lubs RealDef
 begin
 
 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/Rational.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Rational numbers *}
 
 theory Rational
-import Quotient
+imports Quotient
 files ("rat_arith.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
 header{*Defining the Reals from the Positive Reals*}
 
 theory RealDef
-import PReal
+imports PReal
 files ("real_arith.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/RealPow.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory RealPow
-import RealDef
+imports RealDef
 begin
 
 declare abs_mult_self [simp]
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Recdef.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* TFL: recursive function definitions *}
 
 theory Recdef
-import Wellfounded_Relations Datatype
+imports Wellfounded_Relations Datatype
 files
   ("../TFL/utils.ML")
   ("../TFL/usyntax.ML")
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Record.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Record
-import Product_Type
+imports Product_Type
 files ("Tools/record_package.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Refute.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -9,7 +9,7 @@
 header {* Refute *}
 
 theory Refute
-import Map
+imports Map
 files "Tools/prop_logic.ML"
       "Tools/sat_solver.ML"
       "Tools/refute.ML"
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Relation.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Relations *}
 
 theory Relation
-import Product_Type
+imports Product_Type
 begin
 
 subsection {* Definitions *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Relation_Power.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -13,7 +13,7 @@
 *)
 
 theory Relation_Power
-import Nat
+imports Nat
 begin
 
 instance
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* (Ordered) Rings and Fields *}
 
 theory Ring_and_Field 
-import OrderedGroup
+imports OrderedGroup
 begin
 
 text {*
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Set.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* Set theory for higher-order logic *}
 
 theory Set
-import HOL
+imports HOL
 begin
 
 text {* A set in HOL is simply a predicate. *}
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/SetInterval.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -10,7 +10,7 @@
 header {* Set intervals *}
 
 theory SetInterval
-import IntArith
+imports IntArith
 begin
 
 constdefs
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Transitive_Closure.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 header {* Reflexive and Transitive closure of a relation *}
 
 theory Transitive_Closure
-import Inductive
+imports Inductive
 files ("../Provers/trancl.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Typedef.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -6,7 +6,7 @@
 header {* HOL type definitions *}
 
 theory Typedef
-import Set
+imports Set
 files ("Tools/typedef_package.ML")
 begin
 
diff -r 58cd3404cf75 -r 322485b816ac src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/W0/W0.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -3,7 +3,9 @@
     Author:     Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel
 *)
 
-theory W0 = Main:
+theory W0
+imports Main
+begin
 
 section {* Universal error monad *}