import -> imports
authornipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140322485b816ac
parent 15139 58cd3404cf75
child 15141 a95c2ff210ba
import -> imports
src/HOL/Complex/CLim.thy
src/HOL/Complex/CSeries.thy
src/HOL/Complex/CStar.thy
src/HOL/Complex/Complex.thy
src/HOL/Complex/ComplexBin.thy
src/HOL/Complex/Complex_Main.thy
src/HOL/Complex/NSCA.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Extraction.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Gfp.thy
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hyperreal/EvenOdd.thy
src/HOL/Hyperreal/Fact.thy
src/HOL/Hyperreal/Filter.thy
src/HOL/Hyperreal/HLog.thy
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperArith.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Hyperreal.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/Log.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Star.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Inductive.thy
src/HOL/Infinite_Set.thy
src/HOL/Integ/Equiv.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/Numeral.thy
src/HOL/Integ/Parity.thy
src/HOL/Integ/Presburger.thy
src/HOL/LOrder.thy
src/HOL/Lfp.thy
src/HOL/Library/Accessible_Part.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Library.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/Word.thy
src/HOL/Library/Zorn.thy
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/Map.thy
src/HOL/Nat.thy
src/HOL/NatArith.thy
src/HOL/OrderedGroup.thy
src/HOL/Power.thy
src/HOL/PreList.thy
src/HOL/Presburger.thy
src/HOL/Product_Type.thy
src/HOL/Real/Lubs.thy
src/HOL/Real/PReal.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Recdef.thy
src/HOL/Record.thy
src/HOL/Refute.thy
src/HOL/Relation.thy
src/HOL/Relation_Power.thy
src/HOL/Ring_and_Field.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/Transitive_Closure.thy
src/HOL/Typedef.thy
src/HOL/W0/W0.thy
     1.1 --- a/src/HOL/Complex/CLim.thy	Tue Aug 17 11:00:24 2004 +0200
     1.2 +++ b/src/HOL/Complex/CLim.thy	Wed Aug 18 11:09:40 2004 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header{*Limits, Continuity and Differentiation for Complex Functions*}
     1.5  
     1.6  theory CLim
     1.7 -import CSeries
     1.8 +imports CSeries
     1.9  begin
    1.10  
    1.11  (*not in simpset?*)
     2.1 --- a/src/HOL/Complex/CSeries.thy	Tue Aug 17 11:00:24 2004 +0200
     2.2 +++ b/src/HOL/Complex/CSeries.thy	Wed Aug 18 11:09:40 2004 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header{*Finite Summation and Infinite Series for Complex Numbers*}
     2.5  
     2.6  theory CSeries
     2.7 -import CStar
     2.8 +imports CStar
     2.9  begin
    2.10  
    2.11  consts sumc :: "[nat,nat,(nat=>complex)] => complex"
     3.1 --- a/src/HOL/Complex/CStar.thy	Tue Aug 17 11:00:24 2004 +0200
     3.2 +++ b/src/HOL/Complex/CStar.thy	Wed Aug 18 11:09:40 2004 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4        and Complex Functions*}
     3.5  
     3.6  theory CStar
     3.7 -import NSCA
     3.8 +imports NSCA
     3.9  begin
    3.10  
    3.11  constdefs
     4.1 --- a/src/HOL/Complex/Complex.thy	Tue Aug 17 11:00:24 2004 +0200
     4.2 +++ b/src/HOL/Complex/Complex.thy	Wed Aug 18 11:09:40 2004 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  header {* Complex Numbers: Rectangular and Polar Representations *}
     4.5  
     4.6  theory Complex
     4.7 -import "../Hyperreal/HLog"
     4.8 +imports "../Hyperreal/HLog"
     4.9  begin
    4.10  
    4.11  datatype complex = Complex real real
     5.1 --- a/src/HOL/Complex/ComplexBin.thy	Tue Aug 17 11:00:24 2004 +0200
     5.2 +++ b/src/HOL/Complex/ComplexBin.thy	Wed Aug 18 11:09:40 2004 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  *)
     5.5  
     5.6  theory ComplexBin
     5.7 -import Complex
     5.8 +imports Complex
     5.9  begin
    5.10  
    5.11  end
     6.1 --- a/src/HOL/Complex/Complex_Main.thy	Tue Aug 17 11:00:24 2004 +0200
     6.2 +++ b/src/HOL/Complex/Complex_Main.thy	Wed Aug 18 11:09:40 2004 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  header{*Comprehensive Complex Theory*}
     6.5  
     6.6  theory Complex_Main
     6.7 -import CLim
     6.8 +imports CLim
     6.9  begin
    6.10  
    6.11  end
     7.1 --- a/src/HOL/Complex/NSCA.thy	Tue Aug 17 11:00:24 2004 +0200
     7.2 +++ b/src/HOL/Complex/NSCA.thy	Wed Aug 18 11:09:40 2004 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  header{*Non-Standard Complex Analysis*}
     7.5  
     7.6  theory NSCA
     7.7 -import NSComplex
     7.8 +imports NSComplex
     7.9  begin
    7.10  
    7.11  constdefs
     8.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Aug 17 11:00:24 2004 +0200
     8.2 +++ b/src/HOL/Complex/NSComplex.thy	Wed Aug 18 11:09:40 2004 +0200
     8.3 @@ -8,7 +8,7 @@
     8.4  header{*Nonstandard Complex Numbers*}
     8.5  
     8.6  theory NSComplex
     8.7 -import Complex
     8.8 +imports Complex
     8.9  begin
    8.10  
    8.11  constdefs
     9.1 --- a/src/HOL/Datatype.thy	Tue Aug 17 11:00:24 2004 +0200
     9.2 +++ b/src/HOL/Datatype.thy	Wed Aug 18 11:09:40 2004 +0200
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Datatypes *}
     9.5  
     9.6  theory Datatype
     9.7 -import Datatype_Universe
     9.8 +imports Datatype_Universe
     9.9  begin
    9.10  
    9.11  subsection {* Representing primitive types *}
    10.1 --- a/src/HOL/Divides.thy	Tue Aug 17 11:00:24 2004 +0200
    10.2 +++ b/src/HOL/Divides.thy	Wed Aug 18 11:09:40 2004 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  *)
    10.5  
    10.6  theory Divides
    10.7 -import NatArith
    10.8 +imports NatArith
    10.9  begin
   10.10  
   10.11  (*We use the same class for div and mod;
    11.1 --- a/src/HOL/Extraction.thy	Tue Aug 17 11:00:24 2004 +0200
    11.2 +++ b/src/HOL/Extraction.thy	Wed Aug 18 11:09:40 2004 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Program extraction for HOL *}
    11.5  
    11.6  theory Extraction
    11.7 -import Datatype
    11.8 +imports Datatype
    11.9  files "Tools/rewrite_hol_proof.ML"
   11.10  begin
   11.11  
    12.1 --- a/src/HOL/Finite_Set.thy	Tue Aug 17 11:00:24 2004 +0200
    12.2 +++ b/src/HOL/Finite_Set.thy	Wed Aug 18 11:09:40 2004 +0200
    12.3 @@ -7,7 +7,7 @@
    12.4  header {* Finite sets *}
    12.5  
    12.6  theory Finite_Set
    12.7 -import Divides Power Inductive
    12.8 +imports Divides Power Inductive
    12.9  begin
   12.10  
   12.11  subsection {* Collection of finite sets *}
    13.1 --- a/src/HOL/Fun.thy	Tue Aug 17 11:00:24 2004 +0200
    13.2 +++ b/src/HOL/Fun.thy	Wed Aug 18 11:09:40 2004 +0200
    13.3 @@ -7,7 +7,7 @@
    13.4  *)
    13.5  
    13.6  theory Fun 
    13.7 -import Typedef
    13.8 +imports Typedef
    13.9  begin
   13.10  
   13.11  instance set :: (type) order
    14.1 --- a/src/HOL/Gfp.thy	Tue Aug 17 11:00:24 2004 +0200
    14.2 +++ b/src/HOL/Gfp.thy	Wed Aug 18 11:09:40 2004 +0200
    14.3 @@ -7,7 +7,7 @@
    14.4  *)
    14.5  
    14.6  theory Gfp 
    14.7 -import Lfp
    14.8 +imports Lfp
    14.9  begin
   14.10  
   14.11  constdefs
    15.1 --- a/src/HOL/HOL.thy	Tue Aug 17 11:00:24 2004 +0200
    15.2 +++ b/src/HOL/HOL.thy	Wed Aug 18 11:09:40 2004 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  header {* The basis of Higher-Order Logic *}
    15.5  
    15.6  theory HOL
    15.7 -import CPure
    15.8 +imports CPure
    15.9  files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
   15.10  begin
   15.11  
    16.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Aug 17 11:00:24 2004 +0200
    16.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 18 11:09:40 2004 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
    16.5  
    16.6  theory Hilbert_Choice
    16.7 -import NatArith
    16.8 +imports NatArith
    16.9  files ("Tools/meson.ML") ("Tools/specification_package.ML")
   16.10  begin
   16.11  
    17.1 --- a/src/HOL/Hyperreal/EvenOdd.thy	Tue Aug 17 11:00:24 2004 +0200
    17.2 +++ b/src/HOL/Hyperreal/EvenOdd.thy	Wed Aug 18 11:09:40 2004 +0200
    17.3 @@ -7,7 +7,7 @@
    17.4  header{*Even and Odd Numbers: Compatibility file for Parity*}
    17.5  
    17.6  theory EvenOdd
    17.7 -import NthRoot
    17.8 +imports NthRoot
    17.9  begin
   17.10  
   17.11  subsection{*General Lemmas About Division*}
    18.1 --- a/src/HOL/Hyperreal/Fact.thy	Tue Aug 17 11:00:24 2004 +0200
    18.2 +++ b/src/HOL/Hyperreal/Fact.thy	Wed Aug 18 11:09:40 2004 +0200
    18.3 @@ -7,7 +7,7 @@
    18.4  header{*Factorial Function*}
    18.5  
    18.6  theory Fact
    18.7 -import Real
    18.8 +imports Real
    18.9  begin
   18.10  
   18.11  consts fact :: "nat => nat"
    19.1 --- a/src/HOL/Hyperreal/Filter.thy	Tue Aug 17 11:00:24 2004 +0200
    19.2 +++ b/src/HOL/Hyperreal/Filter.thy	Wed Aug 18 11:09:40 2004 +0200
    19.3 @@ -8,7 +8,7 @@
    19.4  header{*Filters and Ultrafilters*}
    19.5  
    19.6  theory Filter
    19.7 -import Zorn
    19.8 +imports Zorn
    19.9  begin
   19.10  
   19.11  constdefs
    20.1 --- a/src/HOL/Hyperreal/HLog.thy	Tue Aug 17 11:00:24 2004 +0200
    20.2 +++ b/src/HOL/Hyperreal/HLog.thy	Wed Aug 18 11:09:40 2004 +0200
    20.3 @@ -6,7 +6,7 @@
    20.4  header{*Logarithms: Non-Standard Version*}
    20.5  
    20.6  theory HLog
    20.7 -import Log HTranscendental
    20.8 +imports Log HTranscendental
    20.9  begin
   20.10  
   20.11  
    21.1 --- a/src/HOL/Hyperreal/HSeries.thy	Tue Aug 17 11:00:24 2004 +0200
    21.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Wed Aug 18 11:09:40 2004 +0200
    21.3 @@ -8,7 +8,7 @@
    21.4  header{*Finite Summation and Infinite Series for Hyperreals*}
    21.5  
    21.6  theory HSeries
    21.7 -import Series
    21.8 +imports Series
    21.9  begin
   21.10  
   21.11  constdefs 
    22.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Tue Aug 17 11:00:24 2004 +0200
    22.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Aug 18 11:09:40 2004 +0200
    22.3 @@ -8,7 +8,7 @@
    22.4  header{*Nonstandard Extensions of Transcendental Functions*}
    22.5  
    22.6  theory HTranscendental
    22.7 -import Transcendental Integration
    22.8 +imports Transcendental Integration
    22.9  begin
   22.10  
   22.11  text{*really belongs in Transcendental*}
    23.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Tue Aug 17 11:00:24 2004 +0200
    23.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Wed Aug 18 11:09:40 2004 +0200
    23.3 @@ -7,7 +7,7 @@
    23.4  header{*Binary arithmetic and Simplification for the Hyperreals*}
    23.5  
    23.6  theory HyperArith
    23.7 -import HyperDef
    23.8 +imports HyperDef
    23.9  files ("hypreal_arith.ML")
   23.10  begin
   23.11  
    24.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Aug 17 11:00:24 2004 +0200
    24.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Aug 18 11:09:40 2004 +0200
    24.3 @@ -8,7 +8,7 @@
    24.4  header{*Construction of Hyperreals Using Ultrafilters*}
    24.5  
    24.6  theory HyperDef
    24.7 -import Filter "../Real/Real"
    24.8 +imports Filter "../Real/Real"
    24.9  files ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
   24.10  begin
   24.11  
    25.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Tue Aug 17 11:00:24 2004 +0200
    25.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Aug 18 11:09:40 2004 +0200
    25.3 @@ -8,7 +8,7 @@
    25.4  header{*Construction of Hypernaturals using Ultrafilters*}
    25.5  
    25.6  theory HyperNat
    25.7 -import Star
    25.8 +imports Star
    25.9  begin
   25.10  
   25.11  constdefs
    26.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Tue Aug 17 11:00:24 2004 +0200
    26.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Aug 18 11:09:40 2004 +0200
    26.3 @@ -7,7 +7,7 @@
    26.4  header{*Exponentials on the Hyperreals*}
    26.5  
    26.6  theory HyperPow
    26.7 -import HyperArith HyperNat "../Real/RealPow"
    26.8 +imports HyperArith HyperNat "../Real/RealPow"
    26.9  begin
   26.10  
   26.11  instance hypreal :: power ..
    27.1 --- a/src/HOL/Hyperreal/Hyperreal.thy	Tue Aug 17 11:00:24 2004 +0200
    27.2 +++ b/src/HOL/Hyperreal/Hyperreal.thy	Wed Aug 18 11:09:40 2004 +0200
    27.3 @@ -8,7 +8,7 @@
    27.4  *)
    27.5  
    27.6  theory Hyperreal
    27.7 -import Poly MacLaurin HLog
    27.8 +imports Poly MacLaurin HLog
    27.9  begin
   27.10  
   27.11  end
    28.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Aug 17 11:00:24 2004 +0200
    28.2 +++ b/src/HOL/Hyperreal/Integration.thy	Wed Aug 18 11:09:40 2004 +0200
    28.3 @@ -7,7 +7,7 @@
    28.4  header{*Theory of Integration*}
    28.5  
    28.6  theory Integration
    28.7 -import MacLaurin
    28.8 +imports MacLaurin
    28.9  begin
   28.10  
   28.11  text{*We follow John Harrison in formalizing the Gauge integral.*}
    29.1 --- a/src/HOL/Hyperreal/Lim.thy	Tue Aug 17 11:00:24 2004 +0200
    29.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed Aug 18 11:09:40 2004 +0200
    29.3 @@ -8,7 +8,7 @@
    29.4  header{*Limits, Continuity and Differentiation*}
    29.5  
    29.6  theory Lim
    29.7 -import SEQ RealDef
    29.8 +imports SEQ RealDef
    29.9  begin
   29.10  
   29.11  text{*Standard and Nonstandard Definitions*}
    30.1 --- a/src/HOL/Hyperreal/Log.thy	Tue Aug 17 11:00:24 2004 +0200
    30.2 +++ b/src/HOL/Hyperreal/Log.thy	Wed Aug 18 11:09:40 2004 +0200
    30.3 @@ -6,7 +6,7 @@
    30.4  header{*Logarithms: Standard Version*}
    30.5  
    30.6  theory Log
    30.7 -import Transcendental
    30.8 +imports Transcendental
    30.9  begin
   30.10  
   30.11  constdefs
    31.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Aug 17 11:00:24 2004 +0200
    31.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Aug 18 11:09:40 2004 +0200
    31.3 @@ -6,7 +6,7 @@
    31.4  *)
    31.5  
    31.6  theory MacLaurin
    31.7 -import Log
    31.8 +imports Log
    31.9  begin
   31.10  
   31.11  lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
    32.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Aug 17 11:00:24 2004 +0200
    32.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Aug 18 11:09:40 2004 +0200
    32.3 @@ -8,7 +8,7 @@
    32.4  header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
    32.5  
    32.6  theory NSA
    32.7 -import HyperArith RComplete
    32.8 +imports HyperArith RComplete
    32.9  begin
   32.10  
   32.11  constdefs
    33.1 --- a/src/HOL/Hyperreal/NatStar.thy	Tue Aug 17 11:00:24 2004 +0200
    33.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Wed Aug 18 11:09:40 2004 +0200
    33.3 @@ -8,7 +8,7 @@
    33.4  header{*Star-transforms for the Hypernaturals*}
    33.5  
    33.6  theory NatStar
    33.7 -import "../Real/RealPow" HyperPow
    33.8 +imports "../Real/RealPow" HyperPow
    33.9  begin
   33.10  
   33.11  text{*Extends sets of nats, and functions from the nats to nats or reals*}
    34.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue Aug 17 11:00:24 2004 +0200
    34.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Aug 18 11:09:40 2004 +0200
    34.3 @@ -7,7 +7,7 @@
    34.4  header{*Existence of Nth Root*}
    34.5  
    34.6  theory NthRoot
    34.7 -import SEQ HSeries
    34.8 +imports SEQ HSeries
    34.9  begin
   34.10  
   34.11  text {*
    35.1 --- a/src/HOL/Hyperreal/Poly.thy	Tue Aug 17 11:00:24 2004 +0200
    35.2 +++ b/src/HOL/Hyperreal/Poly.thy	Wed Aug 18 11:09:40 2004 +0200
    35.3 @@ -9,7 +9,7 @@
    35.4  header{*Univariate Real Polynomials*}
    35.5  
    35.6  theory Poly
    35.7 -import Transcendental
    35.8 +imports Transcendental
    35.9  begin
   35.10  
   35.11  text{*Application of polynomial as a real function.*}
    36.1 --- a/src/HOL/Hyperreal/SEQ.thy	Tue Aug 17 11:00:24 2004 +0200
    36.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Wed Aug 18 11:09:40 2004 +0200
    36.3 @@ -6,7 +6,7 @@
    36.4  *)
    36.5  
    36.6  theory SEQ
    36.7 -import NatStar HyperPow
    36.8 +imports NatStar HyperPow
    36.9  begin
   36.10  
   36.11  constdefs
    37.1 --- a/src/HOL/Hyperreal/Series.thy	Tue Aug 17 11:00:24 2004 +0200
    37.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed Aug 18 11:09:40 2004 +0200
    37.3 @@ -8,7 +8,7 @@
    37.4  header{*Finite Summation and Infinite Series*}
    37.5  
    37.6  theory Series
    37.7 -import SEQ Lim
    37.8 +imports SEQ Lim
    37.9  begin
   37.10  
   37.11  syntax sumr :: "[nat,nat,(nat=>real)] => real"
    38.1 --- a/src/HOL/Hyperreal/Star.thy	Tue Aug 17 11:00:24 2004 +0200
    38.2 +++ b/src/HOL/Hyperreal/Star.thy	Wed Aug 18 11:09:40 2004 +0200
    38.3 @@ -7,7 +7,7 @@
    38.4  header{*Star-Transforms in Non-Standard Analysis*}
    38.5  
    38.6  theory Star
    38.7 -import NSA
    38.8 +imports NSA
    38.9  begin
   38.10  
   38.11  constdefs
    39.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Aug 17 11:00:24 2004 +0200
    39.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Aug 18 11:09:40 2004 +0200
    39.3 @@ -8,7 +8,7 @@
    39.4  header{*Power Series, Transcendental Functions etc.*}
    39.5  
    39.6  theory Transcendental
    39.7 -import NthRoot Fact HSeries EvenOdd Lim
    39.8 +imports NthRoot Fact HSeries EvenOdd Lim
    39.9  begin
   39.10  
   39.11  constdefs
    40.1 --- a/src/HOL/Inductive.thy	Tue Aug 17 11:00:24 2004 +0200
    40.2 +++ b/src/HOL/Inductive.thy	Wed Aug 18 11:09:40 2004 +0200
    40.3 @@ -6,7 +6,7 @@
    40.4  header {* Support for inductive sets and types *}
    40.5  
    40.6  theory Inductive 
    40.7 -import Gfp Sum_Type Relation Record
    40.8 +imports Gfp Sum_Type Relation Record
    40.9  files
   40.10    ("Tools/inductive_package.ML")
   40.11    ("Tools/inductive_realizer.ML")
    41.1 --- a/src/HOL/Infinite_Set.thy	Tue Aug 17 11:00:24 2004 +0200
    41.2 +++ b/src/HOL/Infinite_Set.thy	Wed Aug 18 11:09:40 2004 +0200
    41.3 @@ -6,7 +6,7 @@
    41.4  header {* Infnite Sets and Related Concepts*}
    41.5  
    41.6  theory Infinite_Set
    41.7 -import Hilbert_Choice Finite_Set SetInterval
    41.8 +imports Hilbert_Choice Finite_Set SetInterval
    41.9  begin
   41.10  
   41.11  subsection "Infinite Sets"
    42.1 --- a/src/HOL/Integ/Equiv.thy	Tue Aug 17 11:00:24 2004 +0200
    42.2 +++ b/src/HOL/Integ/Equiv.thy	Wed Aug 18 11:09:40 2004 +0200
    42.3 @@ -7,7 +7,7 @@
    42.4  header {* Equivalence relations in Higher-Order Set Theory *}
    42.5  
    42.6  theory Equiv
    42.7 -import Relation Finite_Set
    42.8 +imports Relation Finite_Set
    42.9  begin
   42.10  
   42.11  subsection {* Equivalence relations *}
    43.1 --- a/src/HOL/Integ/IntArith.thy	Tue Aug 17 11:00:24 2004 +0200
    43.2 +++ b/src/HOL/Integ/IntArith.thy	Wed Aug 18 11:09:40 2004 +0200
    43.3 @@ -6,7 +6,7 @@
    43.4  header {* Integer arithmetic *}
    43.5  
    43.6  theory IntArith
    43.7 -import Numeral
    43.8 +imports Numeral
    43.9  files ("int_arith1.ML")
   43.10  begin
   43.11  
    44.1 --- a/src/HOL/Integ/IntDef.thy	Tue Aug 17 11:00:24 2004 +0200
    44.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Aug 18 11:09:40 2004 +0200
    44.3 @@ -8,7 +8,7 @@
    44.4  header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
    44.5  
    44.6  theory IntDef
    44.7 -import Equiv NatArith
    44.8 +imports Equiv NatArith
    44.9  begin
   44.10  
   44.11  constdefs
    45.1 --- a/src/HOL/Integ/IntDiv.thy	Tue Aug 17 11:00:24 2004 +0200
    45.2 +++ b/src/HOL/Integ/IntDiv.thy	Wed Aug 18 11:09:40 2004 +0200
    45.3 @@ -32,7 +32,7 @@
    45.4  
    45.5  
    45.6  theory IntDiv
    45.7 -import IntArith Recdef
    45.8 +imports IntArith Recdef
    45.9  files ("IntDiv_setup.ML")
   45.10  begin
   45.11  
    46.1 --- a/src/HOL/Integ/NatBin.thy	Tue Aug 17 11:00:24 2004 +0200
    46.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Aug 18 11:09:40 2004 +0200
    46.3 @@ -7,7 +7,7 @@
    46.4  header {* Binary arithmetic for the natural numbers *}
    46.5  
    46.6  theory NatBin
    46.7 -import IntDiv
    46.8 +imports IntDiv
    46.9  begin
   46.10  
   46.11  text {*
    47.1 --- a/src/HOL/Integ/NatSimprocs.thy	Tue Aug 17 11:00:24 2004 +0200
    47.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Wed Aug 18 11:09:40 2004 +0200
    47.3 @@ -6,7 +6,7 @@
    47.4  header {*Simprocs for the Naturals*}
    47.5  
    47.6  theory NatSimprocs
    47.7 -import NatBin
    47.8 +imports NatBin
    47.9  files "int_factor_simprocs.ML" "nat_simprocs.ML"
   47.10  begin
   47.11  
    48.1 --- a/src/HOL/Integ/Numeral.thy	Tue Aug 17 11:00:24 2004 +0200
    48.2 +++ b/src/HOL/Integ/Numeral.thy	Wed Aug 18 11:09:40 2004 +0200
    48.3 @@ -7,7 +7,7 @@
    48.4  header{*Arithmetic on Binary Integers*}
    48.5  
    48.6  theory Numeral
    48.7 -import IntDef
    48.8 +imports IntDef
    48.9  files "Tools/numeral_syntax.ML"
   48.10  begin
   48.11  
    49.1 --- a/src/HOL/Integ/Parity.thy	Tue Aug 17 11:00:24 2004 +0200
    49.2 +++ b/src/HOL/Integ/Parity.thy	Wed Aug 18 11:09:40 2004 +0200
    49.3 @@ -6,7 +6,7 @@
    49.4  header {* Parity: Even and Odd for ints and nats*}
    49.5  
    49.6  theory Parity
    49.7 -import Divides IntDiv NatSimprocs
    49.8 +imports Divides IntDiv NatSimprocs
    49.9  begin
   49.10  
   49.11  axclass even_odd < type
    50.1 --- a/src/HOL/Integ/Presburger.thy	Tue Aug 17 11:00:24 2004 +0200
    50.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Aug 18 11:09:40 2004 +0200
    50.3 @@ -9,7 +9,7 @@
    50.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
    50.5  
    50.6  theory Presburger
    50.7 -import NatSimprocs SetInterval
    50.8 +imports NatSimprocs SetInterval
    50.9  files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
   50.10  begin
   50.11  
    51.1 --- a/src/HOL/LOrder.thy	Tue Aug 17 11:00:24 2004 +0200
    51.2 +++ b/src/HOL/LOrder.thy	Wed Aug 18 11:09:40 2004 +0200
    51.3 @@ -6,7 +6,7 @@
    51.4  header {* Lattice Orders *}
    51.5  
    51.6  theory LOrder
    51.7 -import HOL
    51.8 +imports HOL
    51.9  begin
   51.10  
   51.11  text {*
    52.1 --- a/src/HOL/Lfp.thy	Tue Aug 17 11:00:24 2004 +0200
    52.2 +++ b/src/HOL/Lfp.thy	Wed Aug 18 11:09:40 2004 +0200
    52.3 @@ -7,7 +7,7 @@
    52.4  *)
    52.5  
    52.6  theory Lfp
    52.7 -import Product_Type
    52.8 +imports Product_Type
    52.9  begin
   52.10  
   52.11  constdefs
    53.1 --- a/src/HOL/Library/Accessible_Part.thy	Tue Aug 17 11:00:24 2004 +0200
    53.2 +++ b/src/HOL/Library/Accessible_Part.thy	Wed Aug 18 11:09:40 2004 +0200
    53.3 @@ -7,7 +7,7 @@
    53.4  header {* The accessible part of a relation *}
    53.5  
    53.6  theory Accessible_Part
    53.7 -import Main
    53.8 +imports Main
    53.9  begin
   53.10  
   53.11  subsection {* Inductive definition *}
    54.1 --- a/src/HOL/Library/Continuity.thy	Tue Aug 17 11:00:24 2004 +0200
    54.2 +++ b/src/HOL/Library/Continuity.thy	Wed Aug 18 11:09:40 2004 +0200
    54.3 @@ -6,7 +6,7 @@
    54.4  header {* Continuity and iterations (of set transformers) *}
    54.5  
    54.6  theory Continuity
    54.7 -import Main
    54.8 +imports Main
    54.9  begin
   54.10  
   54.11  subsection "Chains"
    55.1 --- a/src/HOL/Library/FuncSet.thy	Tue Aug 17 11:00:24 2004 +0200
    55.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Aug 18 11:09:40 2004 +0200
    55.3 @@ -6,7 +6,7 @@
    55.4  header {* Pi and Function Sets *}
    55.5  
    55.6  theory FuncSet
    55.7 -import Main
    55.8 +imports Main
    55.9  begin
   55.10  
   55.11  constdefs
    56.1 --- a/src/HOL/Library/Library.thy	Tue Aug 17 11:00:24 2004 +0200
    56.2 +++ b/src/HOL/Library/Library.thy	Wed Aug 18 11:09:40 2004 +0200
    56.3 @@ -1,6 +1,6 @@
    56.4  (*<*)
    56.5  theory Library
    56.6 -import
    56.7 +imports
    56.8    Accessible_Part
    56.9    Continuity
   56.10    FuncSet
    57.1 --- a/src/HOL/Library/List_Prefix.thy	Tue Aug 17 11:00:24 2004 +0200
    57.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Aug 18 11:09:40 2004 +0200
    57.3 @@ -6,7 +6,7 @@
    57.4  header {* List prefixes and postfixes *}
    57.5  
    57.6  theory List_Prefix
    57.7 -import Main
    57.8 +imports Main
    57.9  begin
   57.10  
   57.11  subsection {* Prefix order on lists *}
    58.1 --- a/src/HOL/Library/Multiset.thy	Tue Aug 17 11:00:24 2004 +0200
    58.2 +++ b/src/HOL/Library/Multiset.thy	Wed Aug 18 11:09:40 2004 +0200
    58.3 @@ -6,7 +6,7 @@
    58.4  header {* Multisets *}
    58.5  
    58.6  theory Multiset
    58.7 -import Accessible_Part
    58.8 +imports Accessible_Part
    58.9  begin
   58.10  
   58.11  subsection {* The type of multisets *}
    59.1 --- a/src/HOL/Library/NatPair.thy	Tue Aug 17 11:00:24 2004 +0200
    59.2 +++ b/src/HOL/Library/NatPair.thy	Wed Aug 18 11:09:40 2004 +0200
    59.3 @@ -7,7 +7,7 @@
    59.4  header {* Pairs of Natural Numbers *}
    59.5  
    59.6  theory NatPair
    59.7 -import Main
    59.8 +imports Main
    59.9  begin
   59.10  
   59.11  text{*
    60.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Aug 17 11:00:24 2004 +0200
    60.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Wed Aug 18 11:09:40 2004 +0200
    60.3 @@ -6,7 +6,7 @@
    60.4  header {* Natural numbers with infinity *}
    60.5  
    60.6  theory Nat_Infinity
    60.7 -import Main
    60.8 +imports Main
    60.9  begin
   60.10  
   60.11  subsection "Definitions"
    61.1 --- a/src/HOL/Library/Nested_Environment.thy	Tue Aug 17 11:00:24 2004 +0200
    61.2 +++ b/src/HOL/Library/Nested_Environment.thy	Wed Aug 18 11:09:40 2004 +0200
    61.3 @@ -6,7 +6,7 @@
    61.4  header {* Nested environments *}
    61.5  
    61.6  theory Nested_Environment
    61.7 -import Main
    61.8 +imports Main
    61.9  begin
   61.10  
   61.11  text {*
    62.1 --- a/src/HOL/Library/Permutation.thy	Tue Aug 17 11:00:24 2004 +0200
    62.2 +++ b/src/HOL/Library/Permutation.thy	Wed Aug 18 11:09:40 2004 +0200
    62.3 @@ -5,7 +5,7 @@
    62.4  header {* Permutations *}
    62.5  
    62.6  theory Permutation
    62.7 -import Multiset
    62.8 +imports Multiset
    62.9  begin
   62.10  
   62.11  consts
    63.1 --- a/src/HOL/Library/Primes.thy	Tue Aug 17 11:00:24 2004 +0200
    63.2 +++ b/src/HOL/Library/Primes.thy	Wed Aug 18 11:09:40 2004 +0200
    63.3 @@ -7,7 +7,7 @@
    63.4  header {* The Greatest Common Divisor and Euclid's algorithm *}
    63.5  
    63.6  theory Primes
    63.7 -import Main
    63.8 +imports Main
    63.9  begin
   63.10  
   63.11  text {*
    64.1 --- a/src/HOL/Library/Quotient.thy	Tue Aug 17 11:00:24 2004 +0200
    64.2 +++ b/src/HOL/Library/Quotient.thy	Wed Aug 18 11:09:40 2004 +0200
    64.3 @@ -6,7 +6,7 @@
    64.4  header {* Quotient types *}
    64.5  
    64.6  theory Quotient
    64.7 -import Main
    64.8 +imports Main
    64.9  begin
   64.10  
   64.11  text {*
    65.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Aug 17 11:00:24 2004 +0200
    65.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Aug 18 11:09:40 2004 +0200
    65.3 @@ -7,7 +7,7 @@
    65.4  header {* A general ``while'' combinator *}
    65.5  
    65.6  theory While_Combinator
    65.7 -import Main
    65.8 +imports Main
    65.9  begin
   65.10  
   65.11  text {*
    66.1 --- a/src/HOL/Library/Word.thy	Tue Aug 17 11:00:24 2004 +0200
    66.2 +++ b/src/HOL/Library/Word.thy	Wed Aug 18 11:09:40 2004 +0200
    66.3 @@ -6,7 +6,7 @@
    66.4  header {* Binary Words *}
    66.5  
    66.6  theory Word
    66.7 -import Main
    66.8 +imports Main
    66.9  files "word_setup.ML"
   66.10  begin
   66.11  
    67.1 --- a/src/HOL/Library/Zorn.thy	Tue Aug 17 11:00:24 2004 +0200
    67.2 +++ b/src/HOL/Library/Zorn.thy	Wed Aug 18 11:09:40 2004 +0200
    67.3 @@ -7,7 +7,7 @@
    67.4  header {* Zorn's Lemma *}
    67.5  
    67.6  theory Zorn
    67.7 -import Main
    67.8 +imports Main
    67.9  begin
   67.10  
   67.11  text{*
    68.1 --- a/src/HOL/List.thy	Tue Aug 17 11:00:24 2004 +0200
    68.2 +++ b/src/HOL/List.thy	Wed Aug 18 11:09:40 2004 +0200
    68.3 @@ -6,7 +6,7 @@
    68.4  header {* The datatype of finite lists *}
    68.5  
    68.6  theory List
    68.7 -import PreList
    68.8 +imports PreList
    68.9  begin
   68.10  
   68.11  datatype 'a list =
    69.1 --- a/src/HOL/Main.thy	Tue Aug 17 11:00:24 2004 +0200
    69.2 +++ b/src/HOL/Main.thy	Wed Aug 18 11:09:40 2004 +0200
    69.3 @@ -6,7 +6,7 @@
    69.4  header {* Main HOL *}
    69.5  
    69.6  theory Main
    69.7 -import Map Infinite_Set Extraction Refute
    69.8 +imports Map Infinite_Set Extraction Refute
    69.9  begin
   69.10  
   69.11  text {*
    70.1 --- a/src/HOL/Map.thy	Tue Aug 17 11:00:24 2004 +0200
    70.2 +++ b/src/HOL/Map.thy	Wed Aug 18 11:09:40 2004 +0200
    70.3 @@ -9,7 +9,7 @@
    70.4  header {* Maps *}
    70.5  
    70.6  theory Map
    70.7 -import List
    70.8 +imports List
    70.9  begin
   70.10  
   70.11  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
    71.1 --- a/src/HOL/Nat.thy	Tue Aug 17 11:00:24 2004 +0200
    71.2 +++ b/src/HOL/Nat.thy	Wed Aug 18 11:09:40 2004 +0200
    71.3 @@ -9,7 +9,7 @@
    71.4  header {* Natural numbers *}
    71.5  
    71.6  theory Nat
    71.7 -import Wellfounded_Recursion Ring_and_Field
    71.8 +imports Wellfounded_Recursion Ring_and_Field
    71.9  begin
   71.10  
   71.11  subsection {* Type @{text ind} *}
    72.1 --- a/src/HOL/NatArith.thy	Tue Aug 17 11:00:24 2004 +0200
    72.2 +++ b/src/HOL/NatArith.thy	Wed Aug 18 11:09:40 2004 +0200
    72.3 @@ -6,7 +6,7 @@
    72.4  header {* More arithmetic on natural numbers *}
    72.5  
    72.6  theory NatArith
    72.7 -import Nat
    72.8 +imports Nat
    72.9  files "arith_data.ML"
   72.10  begin
   72.11  
    73.1 --- a/src/HOL/OrderedGroup.thy	Tue Aug 17 11:00:24 2004 +0200
    73.2 +++ b/src/HOL/OrderedGroup.thy	Wed Aug 18 11:09:40 2004 +0200
    73.3 @@ -6,7 +6,7 @@
    73.4  header {* Ordered Groups *}
    73.5  
    73.6  theory OrderedGroup
    73.7 -import Inductive LOrder
    73.8 +imports Inductive LOrder
    73.9  files "../Provers/Arith/abel_cancel.ML"
   73.10  begin
   73.11  
    74.1 --- a/src/HOL/Power.thy	Tue Aug 17 11:00:24 2004 +0200
    74.2 +++ b/src/HOL/Power.thy	Wed Aug 18 11:09:40 2004 +0200
    74.3 @@ -8,7 +8,7 @@
    74.4  header{*Exponentiation and Binomial Coefficients*}
    74.5  
    74.6  theory Power
    74.7 -import Divides
    74.8 +imports Divides
    74.9  begin
   74.10  
   74.11  subsection{*Powers for Arbitrary Semirings*}
    75.1 --- a/src/HOL/PreList.thy	Tue Aug 17 11:00:24 2004 +0200
    75.2 +++ b/src/HOL/PreList.thy	Wed Aug 18 11:09:40 2004 +0200
    75.3 @@ -7,7 +7,7 @@
    75.4  header{*A Basis for Building the Theory of Lists*}
    75.5  
    75.6  theory PreList
    75.7 -import Wellfounded_Relations Presburger Recdef Relation_Power Parity
    75.8 +imports Wellfounded_Relations Presburger Recdef Relation_Power Parity
    75.9  begin
   75.10  
   75.11  text {*
    76.1 --- a/src/HOL/Presburger.thy	Tue Aug 17 11:00:24 2004 +0200
    76.2 +++ b/src/HOL/Presburger.thy	Wed Aug 18 11:09:40 2004 +0200
    76.3 @@ -9,7 +9,7 @@
    76.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
    76.5  
    76.6  theory Presburger
    76.7 -import NatSimprocs SetInterval
    76.8 +imports NatSimprocs SetInterval
    76.9  files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
   76.10  begin
   76.11  
    77.1 --- a/src/HOL/Product_Type.thy	Tue Aug 17 11:00:24 2004 +0200
    77.2 +++ b/src/HOL/Product_Type.thy	Wed Aug 18 11:09:40 2004 +0200
    77.3 @@ -7,7 +7,7 @@
    77.4  header {* Cartesian products *}
    77.5  
    77.6  theory Product_Type
    77.7 -import Fun
    77.8 +imports Fun
    77.9  files ("Tools/split_rule.ML")
   77.10  begin
   77.11  
    78.1 --- a/src/HOL/Real/Lubs.thy	Tue Aug 17 11:00:24 2004 +0200
    78.2 +++ b/src/HOL/Real/Lubs.thy	Wed Aug 18 11:09:40 2004 +0200
    78.3 @@ -7,7 +7,7 @@
    78.4  header{*Definitions of Upper Bounds and Least Upper Bounds*}
    78.5  
    78.6  theory Lubs
    78.7 -import Main
    78.8 +imports Main
    78.9  begin
   78.10  
   78.11  text{*Thanks to suggestions by James Margetson*}
    79.1 --- a/src/HOL/Real/PReal.thy	Tue Aug 17 11:00:24 2004 +0200
    79.2 +++ b/src/HOL/Real/PReal.thy	Wed Aug 18 11:09:40 2004 +0200
    79.3 @@ -8,7 +8,7 @@
    79.4  *)
    79.5  
    79.6  theory PReal
    79.7 -import Rational
    79.8 +imports Rational
    79.9  begin
   79.10  
   79.11  text{*Could be generalized and moved to @{text Ring_and_Field}*}
    80.1 --- a/src/HOL/Real/RComplete.thy	Tue Aug 17 11:00:24 2004 +0200
    80.2 +++ b/src/HOL/Real/RComplete.thy	Wed Aug 18 11:09:40 2004 +0200
    80.3 @@ -9,7 +9,7 @@
    80.4  header{*Completeness of the Reals; Floor and Ceiling Functions*}
    80.5  
    80.6  theory RComplete
    80.7 -import Lubs RealDef
    80.8 +imports Lubs RealDef
    80.9  begin
   80.10  
   80.11  lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
    81.1 --- a/src/HOL/Real/Rational.thy	Tue Aug 17 11:00:24 2004 +0200
    81.2 +++ b/src/HOL/Real/Rational.thy	Wed Aug 18 11:09:40 2004 +0200
    81.3 @@ -6,7 +6,7 @@
    81.4  header {* Rational numbers *}
    81.5  
    81.6  theory Rational
    81.7 -import Quotient
    81.8 +imports Quotient
    81.9  files ("rat_arith.ML")
   81.10  begin
   81.11  
    82.1 --- a/src/HOL/Real/RealDef.thy	Tue Aug 17 11:00:24 2004 +0200
    82.2 +++ b/src/HOL/Real/RealDef.thy	Wed Aug 18 11:09:40 2004 +0200
    82.3 @@ -8,7 +8,7 @@
    82.4  header{*Defining the Reals from the Positive Reals*}
    82.5  
    82.6  theory RealDef
    82.7 -import PReal
    82.8 +imports PReal
    82.9  files ("real_arith.ML")
   82.10  begin
   82.11  
    83.1 --- a/src/HOL/Real/RealPow.thy	Tue Aug 17 11:00:24 2004 +0200
    83.2 +++ b/src/HOL/Real/RealPow.thy	Wed Aug 18 11:09:40 2004 +0200
    83.3 @@ -7,7 +7,7 @@
    83.4  *)
    83.5  
    83.6  theory RealPow
    83.7 -import RealDef
    83.8 +imports RealDef
    83.9  begin
   83.10  
   83.11  declare abs_mult_self [simp]
    84.1 --- a/src/HOL/Recdef.thy	Tue Aug 17 11:00:24 2004 +0200
    84.2 +++ b/src/HOL/Recdef.thy	Wed Aug 18 11:09:40 2004 +0200
    84.3 @@ -6,7 +6,7 @@
    84.4  header {* TFL: recursive function definitions *}
    84.5  
    84.6  theory Recdef
    84.7 -import Wellfounded_Relations Datatype
    84.8 +imports Wellfounded_Relations Datatype
    84.9  files
   84.10    ("../TFL/utils.ML")
   84.11    ("../TFL/usyntax.ML")
    85.1 --- a/src/HOL/Record.thy	Tue Aug 17 11:00:24 2004 +0200
    85.2 +++ b/src/HOL/Record.thy	Wed Aug 18 11:09:40 2004 +0200
    85.3 @@ -4,7 +4,7 @@
    85.4  *)
    85.5  
    85.6  theory Record
    85.7 -import Product_Type
    85.8 +imports Product_Type
    85.9  files ("Tools/record_package.ML")
   85.10  begin
   85.11  
    86.1 --- a/src/HOL/Refute.thy	Tue Aug 17 11:00:24 2004 +0200
    86.2 +++ b/src/HOL/Refute.thy	Wed Aug 18 11:09:40 2004 +0200
    86.3 @@ -9,7 +9,7 @@
    86.4  header {* Refute *}
    86.5  
    86.6  theory Refute
    86.7 -import Map
    86.8 +imports Map
    86.9  files "Tools/prop_logic.ML"
   86.10        "Tools/sat_solver.ML"
   86.11        "Tools/refute.ML"
    87.1 --- a/src/HOL/Relation.thy	Tue Aug 17 11:00:24 2004 +0200
    87.2 +++ b/src/HOL/Relation.thy	Wed Aug 18 11:09:40 2004 +0200
    87.3 @@ -7,7 +7,7 @@
    87.4  header {* Relations *}
    87.5  
    87.6  theory Relation
    87.7 -import Product_Type
    87.8 +imports Product_Type
    87.9  begin
   87.10  
   87.11  subsection {* Definitions *}
    88.1 --- a/src/HOL/Relation_Power.thy	Tue Aug 17 11:00:24 2004 +0200
    88.2 +++ b/src/HOL/Relation_Power.thy	Wed Aug 18 11:09:40 2004 +0200
    88.3 @@ -13,7 +13,7 @@
    88.4  *)
    88.5  
    88.6  theory Relation_Power
    88.7 -import Nat
    88.8 +imports Nat
    88.9  begin
   88.10  
   88.11  instance
    89.1 --- a/src/HOL/Ring_and_Field.thy	Tue Aug 17 11:00:24 2004 +0200
    89.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Aug 18 11:09:40 2004 +0200
    89.3 @@ -6,7 +6,7 @@
    89.4  header {* (Ordered) Rings and Fields *}
    89.5  
    89.6  theory Ring_and_Field 
    89.7 -import OrderedGroup
    89.8 +imports OrderedGroup
    89.9  begin
   89.10  
   89.11  text {*
    90.1 --- a/src/HOL/Set.thy	Tue Aug 17 11:00:24 2004 +0200
    90.2 +++ b/src/HOL/Set.thy	Wed Aug 18 11:09:40 2004 +0200
    90.3 @@ -6,7 +6,7 @@
    90.4  header {* Set theory for higher-order logic *}
    90.5  
    90.6  theory Set
    90.7 -import HOL
    90.8 +imports HOL
    90.9  begin
   90.10  
   90.11  text {* A set in HOL is simply a predicate. *}
    91.1 --- a/src/HOL/SetInterval.thy	Tue Aug 17 11:00:24 2004 +0200
    91.2 +++ b/src/HOL/SetInterval.thy	Wed Aug 18 11:09:40 2004 +0200
    91.3 @@ -10,7 +10,7 @@
    91.4  header {* Set intervals *}
    91.5  
    91.6  theory SetInterval
    91.7 -import IntArith
    91.8 +imports IntArith
    91.9  begin
   91.10  
   91.11  constdefs
    92.1 --- a/src/HOL/Transitive_Closure.thy	Tue Aug 17 11:00:24 2004 +0200
    92.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Aug 18 11:09:40 2004 +0200
    92.3 @@ -7,7 +7,7 @@
    92.4  header {* Reflexive and Transitive closure of a relation *}
    92.5  
    92.6  theory Transitive_Closure
    92.7 -import Inductive
    92.8 +imports Inductive
    92.9  files ("../Provers/trancl.ML")
   92.10  begin
   92.11  
    93.1 --- a/src/HOL/Typedef.thy	Tue Aug 17 11:00:24 2004 +0200
    93.2 +++ b/src/HOL/Typedef.thy	Wed Aug 18 11:09:40 2004 +0200
    93.3 @@ -6,7 +6,7 @@
    93.4  header {* HOL type definitions *}
    93.5  
    93.6  theory Typedef
    93.7 -import Set
    93.8 +imports Set
    93.9  files ("Tools/typedef_package.ML")
   93.10  begin
   93.11  
    94.1 --- a/src/HOL/W0/W0.thy	Tue Aug 17 11:00:24 2004 +0200
    94.2 +++ b/src/HOL/W0/W0.thy	Wed Aug 18 11:09:40 2004 +0200
    94.3 @@ -3,7 +3,9 @@
    94.4      Author:     Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel
    94.5  *)
    94.6  
    94.7 -theory W0 = Main:
    94.8 +theory W0
    94.9 +imports Main
   94.10 +begin
   94.11  
   94.12  section {* Universal error monad *}
   94.13