--- 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?*)
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *}
--- 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;
--- 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
--- 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 *}
--- 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
--- 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
--- 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
--- 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
--- 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*}
--- 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"
--- 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
--- 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
--- 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
--- 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*}
--- 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
--- 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
--- 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
--- 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 ..
--- 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
--- 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.*}
--- 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*}
--- 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
--- 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"
--- 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
--- 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*}
--- 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 {*
--- 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.*}
--- 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
--- 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"
--- 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
--- 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
--- 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")
--- 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"
--- 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 *}
--- 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
--- 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
--- 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
--- 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 {*
--- 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
--- 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
--- 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
--- 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
--- 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 {*
--- 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
--- 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 *}
--- 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"
--- 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
--- 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
--- 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 *}
--- 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 *}
--- 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{*
--- 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"
--- 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 {*
--- 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
--- 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 {*
--- 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 {*
--- 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 {*
--- 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
--- 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{*
--- 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 =
--- 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 {*
--- 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)
--- 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} *}
--- 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
--- 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
--- 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*}
--- 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 {*
--- 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
--- 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
--- 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*}
--- 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}*}
--- 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)"
--- 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
--- 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
--- 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]
--- 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")
--- 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
--- 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"
--- 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 *}
--- 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
--- 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 {*
--- 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. *}
--- 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
--- 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
--- 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
--- 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 *}