New theory header syntax.
authornipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131c69542757a4d
parent 15130 dc6be28d7f4e
child 15132 df2b7976d1e7
New theory header syntax.
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
     1.1 --- a/src/HOL/Complex/CLim.thy	Mon Aug 16 14:21:54 2004 +0200
     1.2 +++ b/src/HOL/Complex/CLim.thy	Mon Aug 16 14:22:27 2004 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  header{*Limits, Continuity and Differentiation for Complex Functions*}
     1.6  
     1.7 -theory CLim = CSeries:
     1.8 +theory CLim
     1.9 +import CSeries
    1.10 +begin
    1.11  
    1.12  (*not in simpset?*)
    1.13  declare hypreal_epsilon_not_zero [simp]
     2.1 --- a/src/HOL/Complex/CSeries.thy	Mon Aug 16 14:21:54 2004 +0200
     2.2 +++ b/src/HOL/Complex/CSeries.thy	Mon Aug 16 14:22:27 2004 +0200
     2.3 @@ -5,7 +5,9 @@
     2.4  
     2.5  header{*Finite Summation and Infinite Series for Complex Numbers*}
     2.6  
     2.7 -theory CSeries = CStar:
     2.8 +theory CSeries
     2.9 +import CStar
    2.10 +begin
    2.11  
    2.12  consts sumc :: "[nat,nat,(nat=>complex)] => complex"
    2.13  primrec
     3.1 --- a/src/HOL/Complex/CStar.thy	Mon Aug 16 14:21:54 2004 +0200
     3.2 +++ b/src/HOL/Complex/CStar.thy	Mon Aug 16 14:22:27 2004 +0200
     3.3 @@ -6,7 +6,9 @@
     3.4  header{*Star-transforms in NSA, Extending Sets of Complex Numbers
     3.5        and Complex Functions*}
     3.6  
     3.7 -theory CStar = NSCA:
     3.8 +theory CStar
     3.9 +import NSCA
    3.10 +begin
    3.11  
    3.12  constdefs
    3.13  
     4.1 --- a/src/HOL/Complex/Complex.thy	Mon Aug 16 14:21:54 2004 +0200
     4.2 +++ b/src/HOL/Complex/Complex.thy	Mon Aug 16 14:22:27 2004 +0200
     4.3 @@ -7,7 +7,9 @@
     4.4  
     4.5  header {* Complex Numbers: Rectangular and Polar Representations *}
     4.6  
     4.7 -theory Complex = "../Hyperreal/HLog":
     4.8 +theory Complex
     4.9 +import "../Hyperreal/HLog"
    4.10 +begin
    4.11  
    4.12  datatype complex = Complex real real
    4.13  
     5.1 --- a/src/HOL/Complex/ComplexBin.thy	Mon Aug 16 14:21:54 2004 +0200
     5.2 +++ b/src/HOL/Complex/ComplexBin.thy	Mon Aug 16 14:22:27 2004 +0200
     5.3 @@ -5,5 +5,9 @@
     5.4                  This case is reduced to that for the reals.
     5.5  *)
     5.6  
     5.7 -theory ComplexBin = Complex:
     5.8 +theory ComplexBin
     5.9 +import Complex
    5.10 +begin
    5.11  
    5.12 +end
    5.13 +
     6.1 --- a/src/HOL/Complex/Complex_Main.thy	Mon Aug 16 14:21:54 2004 +0200
     6.2 +++ b/src/HOL/Complex/Complex_Main.thy	Mon Aug 16 14:22:27 2004 +0200
     6.3 @@ -6,6 +6,8 @@
     6.4  
     6.5  header{*Comprehensive Complex Theory*}
     6.6  
     6.7 -theory Complex_Main = CLim:
     6.8 +theory Complex_Main
     6.9 +import CLim
    6.10 +begin
    6.11  
    6.12  end
     7.1 --- a/src/HOL/Complex/NSCA.thy	Mon Aug 16 14:21:54 2004 +0200
     7.2 +++ b/src/HOL/Complex/NSCA.thy	Mon Aug 16 14:22:27 2004 +0200
     7.3 @@ -5,7 +5,9 @@
     7.4  
     7.5  header{*Non-Standard Complex Analysis*}
     7.6  
     7.7 -theory NSCA = NSComplex:
     7.8 +theory NSCA
     7.9 +import NSComplex
    7.10 +begin
    7.11  
    7.12  constdefs
    7.13  
     8.1 --- a/src/HOL/Complex/NSComplex.thy	Mon Aug 16 14:21:54 2004 +0200
     8.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon Aug 16 14:22:27 2004 +0200
     8.3 @@ -7,7 +7,9 @@
     8.4  
     8.5  header{*Nonstandard Complex Numbers*}
     8.6  
     8.7 -theory NSComplex = Complex:
     8.8 +theory NSComplex
     8.9 +import Complex
    8.10 +begin
    8.11  
    8.12  constdefs
    8.13      hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
     9.1 --- a/src/HOL/Datatype.thy	Mon Aug 16 14:21:54 2004 +0200
     9.2 +++ b/src/HOL/Datatype.thy	Mon Aug 16 14:22:27 2004 +0200
     9.3 @@ -5,7 +5,9 @@
     9.4  
     9.5  header {* Datatypes *}
     9.6  
     9.7 -theory Datatype = Datatype_Universe:
     9.8 +theory Datatype
     9.9 +import Datatype_Universe
    9.10 +begin
    9.11  
    9.12  subsection {* Representing primitive types *}
    9.13  
    10.1 --- a/src/HOL/Divides.thy	Mon Aug 16 14:21:54 2004 +0200
    10.2 +++ b/src/HOL/Divides.thy	Mon Aug 16 14:22:27 2004 +0200
    10.3 @@ -6,7 +6,9 @@
    10.4  The division operators div, mod and the divides relation "dvd"
    10.5  *)
    10.6  
    10.7 -theory Divides = NatArith:
    10.8 +theory Divides
    10.9 +import NatArith
   10.10 +begin
   10.11  
   10.12  (*We use the same class for div and mod;
   10.13    moreover, dvd is defined whenever multiplication is*)
    11.1 --- a/src/HOL/Extraction.thy	Mon Aug 16 14:21:54 2004 +0200
    11.2 +++ b/src/HOL/Extraction.thy	Mon Aug 16 14:22:27 2004 +0200
    11.3 @@ -5,9 +5,10 @@
    11.4  
    11.5  header {* Program extraction for HOL *}
    11.6  
    11.7 -theory Extraction = Datatype
    11.8 -files
    11.9 -  "Tools/rewrite_hol_proof.ML":
   11.10 +theory Extraction
   11.11 +import Datatype
   11.12 +files "Tools/rewrite_hol_proof.ML"
   11.13 +begin
   11.14  
   11.15  subsection {* Setup *}
   11.16  
    12.1 --- a/src/HOL/Finite_Set.thy	Mon Aug 16 14:21:54 2004 +0200
    12.2 +++ b/src/HOL/Finite_Set.thy	Mon Aug 16 14:22:27 2004 +0200
    12.3 @@ -6,7 +6,9 @@
    12.4  
    12.5  header {* Finite sets *}
    12.6  
    12.7 -theory Finite_Set = Divides + Power + Inductive:
    12.8 +theory Finite_Set
    12.9 +import Divides Power Inductive
   12.10 +begin
   12.11  
   12.12  subsection {* Collection of finite sets *}
   12.13  
    13.1 --- a/src/HOL/Fun.thy	Mon Aug 16 14:21:54 2004 +0200
    13.2 +++ b/src/HOL/Fun.thy	Mon Aug 16 14:22:27 2004 +0200
    13.3 @@ -6,7 +6,9 @@
    13.4  Notions about functions.
    13.5  *)
    13.6  
    13.7 -theory Fun = Typedef:
    13.8 +theory Fun 
    13.9 +import Typedef
   13.10 +begin
   13.11  
   13.12  instance set :: (type) order
   13.13    by (intro_classes,
    14.1 --- a/src/HOL/Gfp.thy	Mon Aug 16 14:21:54 2004 +0200
    14.2 +++ b/src/HOL/Gfp.thy	Mon Aug 16 14:22:27 2004 +0200
    14.3 @@ -6,7 +6,9 @@
    14.4  Greatest fixed points (requires Lfp too!)
    14.5  *)
    14.6  
    14.7 -theory Gfp = Lfp:
    14.8 +theory Gfp 
    14.9 +import Lfp
   14.10 +begin
   14.11  
   14.12  constdefs
   14.13    gfp :: "['a set=>'a set] => 'a set"
    15.1 --- a/src/HOL/HOL.thy	Mon Aug 16 14:21:54 2004 +0200
    15.2 +++ b/src/HOL/HOL.thy	Mon Aug 16 14:22:27 2004 +0200
    15.3 @@ -5,9 +5,10 @@
    15.4  
    15.5  header {* The basis of Higher-Order Logic *}
    15.6  
    15.7 -theory HOL = CPure
    15.8 -files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
    15.9 -
   15.10 +theory HOL
   15.11 +import CPure
   15.12 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
   15.13 +begin
   15.14  
   15.15  subsection {* Primitive logic *}
   15.16  
    16.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Aug 16 14:21:54 2004 +0200
    16.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Aug 16 14:22:27 2004 +0200
    16.3 @@ -6,9 +6,10 @@
    16.4  
    16.5  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
    16.6  
    16.7 -theory Hilbert_Choice = NatArith
    16.8 -files ("Tools/meson.ML") ("Tools/specification_package.ML"):
    16.9 -
   16.10 +theory Hilbert_Choice
   16.11 +import NatArith
   16.12 +files ("Tools/meson.ML") ("Tools/specification_package.ML")
   16.13 +begin
   16.14  
   16.15  subsection {* Hilbert's epsilon *}
   16.16  
    17.1 --- a/src/HOL/Hyperreal/EvenOdd.thy	Mon Aug 16 14:21:54 2004 +0200
    17.2 +++ b/src/HOL/Hyperreal/EvenOdd.thy	Mon Aug 16 14:22:27 2004 +0200
    17.3 @@ -6,7 +6,9 @@
    17.4  
    17.5  header{*Even and Odd Numbers: Compatibility file for Parity*}
    17.6  
    17.7 -theory EvenOdd = NthRoot:
    17.8 +theory EvenOdd
    17.9 +import NthRoot
   17.10 +begin
   17.11  
   17.12  subsection{*General Lemmas About Division*}
   17.13  
    18.1 --- a/src/HOL/Hyperreal/Fact.thy	Mon Aug 16 14:21:54 2004 +0200
    18.2 +++ b/src/HOL/Hyperreal/Fact.thy	Mon Aug 16 14:22:27 2004 +0200
    18.3 @@ -6,7 +6,9 @@
    18.4  
    18.5  header{*Factorial Function*}
    18.6  
    18.7 -theory Fact = Real:
    18.8 +theory Fact
    18.9 +import Real
   18.10 +begin
   18.11  
   18.12  consts fact :: "nat => nat"
   18.13  primrec
   18.14 @@ -71,4 +73,4 @@
   18.15  by (case_tac "m", auto)
   18.16  
   18.17  
   18.18 -end
   18.19 \ No newline at end of file
   18.20 +end
    19.1 --- a/src/HOL/Hyperreal/Filter.thy	Mon Aug 16 14:21:54 2004 +0200
    19.2 +++ b/src/HOL/Hyperreal/Filter.thy	Mon Aug 16 14:22:27 2004 +0200
    19.3 @@ -7,7 +7,9 @@
    19.4  
    19.5  header{*Filters and Ultrafilters*}
    19.6  
    19.7 -theory Filter = Zorn:
    19.8 +theory Filter
    19.9 +import Zorn
   19.10 +begin
   19.11  
   19.12  constdefs
   19.13  
    20.1 --- a/src/HOL/Hyperreal/HLog.thy	Mon Aug 16 14:21:54 2004 +0200
    20.2 +++ b/src/HOL/Hyperreal/HLog.thy	Mon Aug 16 14:22:27 2004 +0200
    20.3 @@ -5,7 +5,9 @@
    20.4  
    20.5  header{*Logarithms: Non-Standard Version*}
    20.6  
    20.7 -theory HLog = Log + HTranscendental: 
    20.8 +theory HLog
    20.9 +import Log HTranscendental
   20.10 +begin
   20.11  
   20.12  
   20.13  (* should be in NSA.ML *)
    21.1 --- a/src/HOL/Hyperreal/HSeries.thy	Mon Aug 16 14:21:54 2004 +0200
    21.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Mon Aug 16 14:22:27 2004 +0200
    21.3 @@ -7,7 +7,9 @@
    21.4  
    21.5  header{*Finite Summation and Infinite Series for Hyperreals*}
    21.6  
    21.7 -theory HSeries = Series:
    21.8 +theory HSeries
    21.9 +import Series
   21.10 +begin
   21.11  
   21.12  constdefs 
   21.13    sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
    22.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Aug 16 14:21:54 2004 +0200
    22.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Aug 16 14:22:27 2004 +0200
    22.3 @@ -7,7 +7,9 @@
    22.4  
    22.5  header{*Nonstandard Extensions of Transcendental Functions*}
    22.6  
    22.7 -theory HTranscendental = Transcendental + Integration:
    22.8 +theory HTranscendental
    22.9 +import Transcendental Integration
   22.10 +begin
   22.11  
   22.12  text{*really belongs in Transcendental*}
   22.13  lemma sqrt_divide_self_eq:
    23.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Mon Aug 16 14:21:54 2004 +0200
    23.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Mon Aug 16 14:22:27 2004 +0200
    23.3 @@ -6,9 +6,10 @@
    23.4  
    23.5  header{*Binary arithmetic and Simplification for the Hyperreals*}
    23.6  
    23.7 -theory HyperArith = HyperDef
    23.8 -files ("hypreal_arith.ML"):
    23.9 -
   23.10 +theory HyperArith
   23.11 +import HyperDef
   23.12 +files ("hypreal_arith.ML")
   23.13 +begin
   23.14  
   23.15  subsection{*Numerals and Arithmetic*}
   23.16  
    24.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Aug 16 14:21:54 2004 +0200
    24.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Aug 16 14:22:27 2004 +0200
    24.3 @@ -7,9 +7,10 @@
    24.4  
    24.5  header{*Construction of Hyperreals Using Ultrafilters*}
    24.6  
    24.7 -theory HyperDef = Filter + "../Real/Real"
    24.8 -files ("fuf.ML"):  (*Warning: file fuf.ML refers to the name Hyperdef!*)
    24.9 -
   24.10 +theory HyperDef
   24.11 +import Filter "../Real/Real"
   24.12 +files ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
   24.13 +begin
   24.14  
   24.15  constdefs
   24.16  
    25.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Mon Aug 16 14:21:54 2004 +0200
    25.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Aug 16 14:22:27 2004 +0200
    25.3 @@ -7,7 +7,9 @@
    25.4  
    25.5  header{*Construction of Hypernaturals using Ultrafilters*}
    25.6  
    25.7 -theory HyperNat = Star:
    25.8 +theory HyperNat
    25.9 +import Star
   25.10 +begin
   25.11  
   25.12  constdefs
   25.13      hypnatrel :: "((nat=>nat)*(nat=>nat)) set"
    26.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Mon Aug 16 14:21:54 2004 +0200
    26.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Aug 16 14:22:27 2004 +0200
    26.3 @@ -6,7 +6,9 @@
    26.4  
    26.5  header{*Exponentials on the Hyperreals*}
    26.6  
    26.7 -theory HyperPow = HyperArith + HyperNat + "../Real/RealPow":
    26.8 +theory HyperPow
    26.9 +import HyperArith HyperNat "../Real/RealPow"
   26.10 +begin
   26.11  
   26.12  instance hypreal :: power ..
   26.13  
    27.1 --- a/src/HOL/Hyperreal/Hyperreal.thy	Mon Aug 16 14:21:54 2004 +0200
    27.2 +++ b/src/HOL/Hyperreal/Hyperreal.thy	Mon Aug 16 14:22:27 2004 +0200
    27.3 @@ -7,6 +7,8 @@
    27.4  and mechanization of Nonstandard Real Analysis
    27.5  *)
    27.6  
    27.7 -theory Hyperreal = Poly + MacLaurin + HLog:
    27.8 +theory Hyperreal
    27.9 +import Poly MacLaurin HLog
   27.10 +begin
   27.11  
   27.12  end
    28.1 --- a/src/HOL/Hyperreal/Integration.thy	Mon Aug 16 14:21:54 2004 +0200
    28.2 +++ b/src/HOL/Hyperreal/Integration.thy	Mon Aug 16 14:22:27 2004 +0200
    28.3 @@ -6,7 +6,9 @@
    28.4  
    28.5  header{*Theory of Integration*}
    28.6  
    28.7 -theory Integration = MacLaurin:
    28.8 +theory Integration
    28.9 +import MacLaurin
   28.10 +begin
   28.11  
   28.12  text{*We follow John Harrison in formalizing the Gauge integral.*}
   28.13  
    29.1 --- a/src/HOL/Hyperreal/Lim.thy	Mon Aug 16 14:21:54 2004 +0200
    29.2 +++ b/src/HOL/Hyperreal/Lim.thy	Mon Aug 16 14:22:27 2004 +0200
    29.3 @@ -7,7 +7,9 @@
    29.4  
    29.5  header{*Limits, Continuity and Differentiation*}
    29.6  
    29.7 -theory Lim = SEQ + RealDef:
    29.8 +theory Lim
    29.9 +import SEQ RealDef
   29.10 +begin
   29.11  
   29.12  text{*Standard and Nonstandard Definitions*}
   29.13  
    30.1 --- a/src/HOL/Hyperreal/Log.thy	Mon Aug 16 14:21:54 2004 +0200
    30.2 +++ b/src/HOL/Hyperreal/Log.thy	Mon Aug 16 14:22:27 2004 +0200
    30.3 @@ -5,7 +5,9 @@
    30.4  
    30.5  header{*Logarithms: Standard Version*}
    30.6  
    30.7 -theory Log = Transcendental:
    30.8 +theory Log
    30.9 +import Transcendental
   30.10 +begin
   30.11  
   30.12  constdefs
   30.13  
    31.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Aug 16 14:21:54 2004 +0200
    31.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Aug 16 14:22:27 2004 +0200
    31.3 @@ -5,7 +5,9 @@
    31.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    31.5  *)
    31.6  
    31.7 -theory MacLaurin = Log:
    31.8 +theory MacLaurin
    31.9 +import Log
   31.10 +begin
   31.11  
   31.12  lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
   31.13  by (induct_tac "n", auto)
    32.1 --- a/src/HOL/Hyperreal/NSA.thy	Mon Aug 16 14:21:54 2004 +0200
    32.2 +++ b/src/HOL/Hyperreal/NSA.thy	Mon Aug 16 14:22:27 2004 +0200
    32.3 @@ -7,7 +7,9 @@
    32.4  
    32.5  header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
    32.6  
    32.7 -theory NSA = HyperArith + RComplete:
    32.8 +theory NSA
    32.9 +import HyperArith RComplete
   32.10 +begin
   32.11  
   32.12  constdefs
   32.13  
    33.1 --- a/src/HOL/Hyperreal/NatStar.thy	Mon Aug 16 14:21:54 2004 +0200
    33.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Mon Aug 16 14:22:27 2004 +0200
    33.3 @@ -7,8 +7,9 @@
    33.4  
    33.5  header{*Star-transforms for the Hypernaturals*}
    33.6  
    33.7 -theory NatStar = "../Real/RealPow" + HyperPow:
    33.8 -
    33.9 +theory NatStar
   33.10 +import "../Real/RealPow" HyperPow
   33.11 +begin
   33.12  
   33.13  text{*Extends sets of nats, and functions from the nats to nats or reals*}
   33.14  
    34.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Mon Aug 16 14:21:54 2004 +0200
    34.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Mon Aug 16 14:22:27 2004 +0200
    34.3 @@ -6,7 +6,9 @@
    34.4  
    34.5  header{*Existence of Nth Root*}
    34.6  
    34.7 -theory NthRoot = SEQ + HSeries:
    34.8 +theory NthRoot
    34.9 +import SEQ HSeries
   34.10 +begin
   34.11  
   34.12  text {*
   34.13    Various lemmas needed for this result. We follow the proof given by
    35.1 --- a/src/HOL/Hyperreal/Poly.thy	Mon Aug 16 14:21:54 2004 +0200
    35.2 +++ b/src/HOL/Hyperreal/Poly.thy	Mon Aug 16 14:22:27 2004 +0200
    35.3 @@ -8,8 +8,9 @@
    35.4  
    35.5  header{*Univariate Real Polynomials*}
    35.6  
    35.7 -theory Poly = Transcendental:
    35.8 -
    35.9 +theory Poly
   35.10 +import Transcendental
   35.11 +begin
   35.12  
   35.13  text{*Application of polynomial as a real function.*}
   35.14  
    36.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Aug 16 14:21:54 2004 +0200
    36.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon Aug 16 14:22:27 2004 +0200
    36.3 @@ -5,7 +5,9 @@
    36.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    36.5  *)
    36.6  
    36.7 -theory SEQ = NatStar + HyperPow:
    36.8 +theory SEQ
    36.9 +import NatStar HyperPow
   36.10 +begin
   36.11  
   36.12  constdefs
   36.13  
    37.1 --- a/src/HOL/Hyperreal/Series.thy	Mon Aug 16 14:21:54 2004 +0200
    37.2 +++ b/src/HOL/Hyperreal/Series.thy	Mon Aug 16 14:22:27 2004 +0200
    37.3 @@ -7,7 +7,9 @@
    37.4  
    37.5  header{*Finite Summation and Infinite Series*}
    37.6  
    37.7 -theory Series = SEQ + Lim:
    37.8 +theory Series
    37.9 +import SEQ Lim
   37.10 +begin
   37.11  
   37.12  syntax sumr :: "[nat,nat,(nat=>real)] => real"
   37.13  translations
    38.1 --- a/src/HOL/Hyperreal/Star.thy	Mon Aug 16 14:21:54 2004 +0200
    38.2 +++ b/src/HOL/Hyperreal/Star.thy	Mon Aug 16 14:22:27 2004 +0200
    38.3 @@ -6,7 +6,9 @@
    38.4  
    38.5  header{*Star-Transforms in Non-Standard Analysis*}
    38.6  
    38.7 -theory Star = NSA:
    38.8 +theory Star
    38.9 +import NSA
   38.10 +begin
   38.11  
   38.12  constdefs
   38.13      (* nonstandard extension of sets *)
    39.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon Aug 16 14:21:54 2004 +0200
    39.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Aug 16 14:22:27 2004 +0200
    39.3 @@ -7,7 +7,9 @@
    39.4  
    39.5  header{*Power Series, Transcendental Functions etc.*}
    39.6  
    39.7 -theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:
    39.8 +theory Transcendental
    39.9 +import NthRoot Fact HSeries EvenOdd Lim
   39.10 +begin
   39.11  
   39.12  constdefs
   39.13      root :: "[nat,real] => real"
    40.1 --- a/src/HOL/Inductive.thy	Mon Aug 16 14:21:54 2004 +0200
    40.2 +++ b/src/HOL/Inductive.thy	Mon Aug 16 14:22:27 2004 +0200
    40.3 @@ -5,7 +5,8 @@
    40.4  
    40.5  header {* Support for inductive sets and types *}
    40.6  
    40.7 -theory Inductive = Gfp + Sum_Type + Relation + Record
    40.8 +theory Inductive 
    40.9 +import Gfp Sum_Type Relation Record
   40.10  files
   40.11    ("Tools/inductive_package.ML")
   40.12    ("Tools/inductive_realizer.ML")
   40.13 @@ -18,8 +19,8 @@
   40.14    ("Tools/datatype_package.ML")
   40.15    ("Tools/datatype_codegen.ML")
   40.16    ("Tools/recfun_codegen.ML")
   40.17 -  ("Tools/primrec_package.ML"):
   40.18 -
   40.19 +  ("Tools/primrec_package.ML")
   40.20 +begin
   40.21  
   40.22  subsection {* Inductive sets *}
   40.23  
    41.1 --- a/src/HOL/Infinite_Set.thy	Mon Aug 16 14:21:54 2004 +0200
    41.2 +++ b/src/HOL/Infinite_Set.thy	Mon Aug 16 14:22:27 2004 +0200
    41.3 @@ -5,7 +5,9 @@
    41.4  
    41.5  header {* Infnite Sets and Related Concepts*}
    41.6  
    41.7 -theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval:
    41.8 +theory Infinite_Set
    41.9 +import Hilbert_Choice Finite_Set SetInterval
   41.10 +begin
   41.11  
   41.12  subsection "Infinite Sets"
   41.13  
    42.1 --- a/src/HOL/Integ/Equiv.thy	Mon Aug 16 14:21:54 2004 +0200
    42.2 +++ b/src/HOL/Integ/Equiv.thy	Mon Aug 16 14:22:27 2004 +0200
    42.3 @@ -6,7 +6,9 @@
    42.4  
    42.5  header {* Equivalence relations in Higher-Order Set Theory *}
    42.6  
    42.7 -theory Equiv = Relation + Finite_Set:
    42.8 +theory Equiv
    42.9 +import Relation Finite_Set
   42.10 +begin
   42.11  
   42.12  subsection {* Equivalence relations *}
   42.13  
    43.1 --- a/src/HOL/Integ/IntArith.thy	Mon Aug 16 14:21:54 2004 +0200
    43.2 +++ b/src/HOL/Integ/IntArith.thy	Mon Aug 16 14:22:27 2004 +0200
    43.3 @@ -5,8 +5,10 @@
    43.4  
    43.5  header {* Integer arithmetic *}
    43.6  
    43.7 -theory IntArith = Numeral
    43.8 -files ("int_arith1.ML"):
    43.9 +theory IntArith
   43.10 +import Numeral
   43.11 +files ("int_arith1.ML")
   43.12 +begin
   43.13  
   43.14  text{*Duplicate: can't understand why it's necessary*}
   43.15  declare numeral_0_eq_0 [simp]
    44.1 --- a/src/HOL/Integ/IntDef.thy	Mon Aug 16 14:21:54 2004 +0200
    44.2 +++ b/src/HOL/Integ/IntDef.thy	Mon Aug 16 14:22:27 2004 +0200
    44.3 @@ -7,7 +7,9 @@
    44.4  
    44.5  header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
    44.6  
    44.7 -theory IntDef = Equiv + NatArith:
    44.8 +theory IntDef
    44.9 +import Equiv NatArith
   44.10 +begin
   44.11  
   44.12  constdefs
   44.13    intrel :: "((nat * nat) * (nat * nat)) set"
    45.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Aug 16 14:21:54 2004 +0200
    45.2 +++ b/src/HOL/Integ/IntDiv.thy	Mon Aug 16 14:22:27 2004 +0200
    45.3 @@ -31,8 +31,10 @@
    45.4  *)
    45.5  
    45.6  
    45.7 -theory IntDiv = IntArith + Recdef
    45.8 -  files ("IntDiv_setup.ML"):
    45.9 +theory IntDiv
   45.10 +import IntArith Recdef
   45.11 +files ("IntDiv_setup.ML")
   45.12 +begin
   45.13  
   45.14  declare zless_nat_conj [simp]
   45.15  
    46.1 --- a/src/HOL/Integ/NatBin.thy	Mon Aug 16 14:21:54 2004 +0200
    46.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Aug 16 14:22:27 2004 +0200
    46.3 @@ -6,7 +6,9 @@
    46.4  
    46.5  header {* Binary arithmetic for the natural numbers *}
    46.6  
    46.7 -theory NatBin = IntDiv:
    46.8 +theory NatBin
    46.9 +import IntDiv
   46.10 +begin
   46.11  
   46.12  text {*
   46.13    Arithmetic for naturals is reduced to that for the non-negative integers.
    47.1 --- a/src/HOL/Integ/NatSimprocs.thy	Mon Aug 16 14:21:54 2004 +0200
    47.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Mon Aug 16 14:22:27 2004 +0200
    47.3 @@ -5,8 +5,10 @@
    47.4  
    47.5  header {*Simprocs for the Naturals*}
    47.6  
    47.7 -theory NatSimprocs = NatBin
    47.8 -files "int_factor_simprocs.ML" "nat_simprocs.ML":
    47.9 +theory NatSimprocs
   47.10 +import NatBin
   47.11 +files "int_factor_simprocs.ML" "nat_simprocs.ML"
   47.12 +begin
   47.13  
   47.14  setup nat_simprocs_setup
   47.15  
    48.1 --- a/src/HOL/Integ/Numeral.thy	Mon Aug 16 14:21:54 2004 +0200
    48.2 +++ b/src/HOL/Integ/Numeral.thy	Mon Aug 16 14:22:27 2004 +0200
    48.3 @@ -6,8 +6,10 @@
    48.4  
    48.5  header{*Arithmetic on Binary Integers*}
    48.6  
    48.7 -theory Numeral = IntDef
    48.8 -files "Tools/numeral_syntax.ML":
    48.9 +theory Numeral
   48.10 +import IntDef
   48.11 +files "Tools/numeral_syntax.ML"
   48.12 +begin
   48.13  
   48.14  text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
   48.15     Only qualified access Numeral.Pls and Numeral.Min is allowed.
    49.1 --- a/src/HOL/Integ/Parity.thy	Mon Aug 16 14:21:54 2004 +0200
    49.2 +++ b/src/HOL/Integ/Parity.thy	Mon Aug 16 14:22:27 2004 +0200
    49.3 @@ -5,7 +5,9 @@
    49.4  
    49.5  header {* Parity: Even and Odd for ints and nats*}
    49.6  
    49.7 -theory Parity = Divides + IntDiv + NatSimprocs:
    49.8 +theory Parity
    49.9 +import Divides IntDiv NatSimprocs
   49.10 +begin
   49.11  
   49.12  axclass even_odd < type
   49.13  
    50.1 --- a/src/HOL/Integ/Presburger.thy	Mon Aug 16 14:21:54 2004 +0200
    50.2 +++ b/src/HOL/Integ/Presburger.thy	Mon Aug 16 14:22:27 2004 +0200
    50.3 @@ -6,14 +6,12 @@
    50.4  generation for Cooper Algorithm  
    50.5  *)
    50.6  
    50.7 -header {* Presburger Arithmetic: Cooper Algorithm *}
    50.8 +header {* Presburger Arithmetic: Cooper's Algorithm *}
    50.9  
   50.10 -theory Presburger = NatSimprocs + SetInterval
   50.11 -files
   50.12 -  ("cooper_dec.ML")
   50.13 -  ("cooper_proof.ML")
   50.14 -  ("qelim.ML")
   50.15 -  ("presburger.ML"):
   50.16 +theory Presburger
   50.17 +import NatSimprocs SetInterval
   50.18 +files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
   50.19 +begin
   50.20  
   50.21  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
   50.22  
    51.1 --- a/src/HOL/LOrder.thy	Mon Aug 16 14:21:54 2004 +0200
    51.2 +++ b/src/HOL/LOrder.thy	Mon Aug 16 14:22:27 2004 +0200
    51.3 @@ -5,7 +5,9 @@
    51.4  
    51.5  header {* Lattice Orders *}
    51.6  
    51.7 -theory LOrder = HOL:
    51.8 +theory LOrder
    51.9 +import HOL
   51.10 +begin
   51.11  
   51.12  text {*
   51.13    The theory of lattices developed here is taken from the book:
   51.14 @@ -327,4 +329,4 @@
   51.15  val modular_le = thm "modular_le";
   51.16  *}
   51.17  
   51.18 -end
   51.19 \ No newline at end of file
   51.20 +end
    52.1 --- a/src/HOL/Lfp.thy	Mon Aug 16 14:21:54 2004 +0200
    52.2 +++ b/src/HOL/Lfp.thy	Mon Aug 16 14:22:27 2004 +0200
    52.3 @@ -6,7 +6,9 @@
    52.4  The Knaster-Tarski Theorem
    52.5  *)
    52.6  
    52.7 -theory Lfp = Product_Type:
    52.8 +theory Lfp
    52.9 +import Product_Type
   52.10 +begin
   52.11  
   52.12  constdefs
   52.13    lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
    53.1 --- a/src/HOL/Library/Accessible_Part.thy	Mon Aug 16 14:21:54 2004 +0200
    53.2 +++ b/src/HOL/Library/Accessible_Part.thy	Mon Aug 16 14:22:27 2004 +0200
    53.3 @@ -6,8 +6,9 @@
    53.4  
    53.5  header {* The accessible part of a relation *}
    53.6  
    53.7 -theory Accessible_Part = Main:
    53.8 -
    53.9 +theory Accessible_Part
   53.10 +import Main
   53.11 +begin
   53.12  
   53.13  subsection {* Inductive definition *}
   53.14  
    54.1 --- a/src/HOL/Library/Continuity.thy	Mon Aug 16 14:21:54 2004 +0200
    54.2 +++ b/src/HOL/Library/Continuity.thy	Mon Aug 16 14:22:27 2004 +0200
    54.3 @@ -5,7 +5,9 @@
    54.4  
    54.5  header {* Continuity and iterations (of set transformers) *}
    54.6  
    54.7 -theory Continuity = Main:
    54.8 +theory Continuity
    54.9 +import Main
   54.10 +begin
   54.11  
   54.12  subsection "Chains"
   54.13  
    55.1 --- a/src/HOL/Library/FuncSet.thy	Mon Aug 16 14:21:54 2004 +0200
    55.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Aug 16 14:22:27 2004 +0200
    55.3 @@ -5,7 +5,9 @@
    55.4  
    55.5  header {* Pi and Function Sets *}
    55.6  
    55.7 -theory FuncSet = Main:
    55.8 +theory FuncSet
    55.9 +import Main
   55.10 +begin
   55.11  
   55.12  constdefs
   55.13    Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
    56.1 --- a/src/HOL/Library/Library.thy	Mon Aug 16 14:21:54 2004 +0200
    56.2 +++ b/src/HOL/Library/Library.thy	Mon Aug 16 14:22:27 2004 +0200
    56.3 @@ -1,18 +1,20 @@
    56.4  (*<*)
    56.5 -theory Library =
    56.6 -  Accessible_Part +
    56.7 -  Continuity +
    56.8 -  FuncSet +
    56.9 -  List_Prefix +
   56.10 -  Multiset +
   56.11 -  NatPair +
   56.12 -  Nat_Infinity +
   56.13 -  Nested_Environment +
   56.14 -  Permutation +
   56.15 -  Primes +
   56.16 -  Quotient +
   56.17 -  While_Combinator +
   56.18 -  Word +
   56.19 -  Zorn:
   56.20 +theory Library
   56.21 +import
   56.22 +  Accessible_Part
   56.23 +  Continuity
   56.24 +  FuncSet
   56.25 +  List_Prefix
   56.26 +  Multiset
   56.27 +  NatPair
   56.28 +  Nat_Infinity
   56.29 +  Nested_Environment
   56.30 +  Permutation
   56.31 +  Primes
   56.32 +  Quotient
   56.33 +  While_Combinator
   56.34 +  Word
   56.35 +  Zorn
   56.36 +begin
   56.37  end
   56.38  (*>*)
    57.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Aug 16 14:21:54 2004 +0200
    57.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Aug 16 14:22:27 2004 +0200
    57.3 @@ -5,7 +5,9 @@
    57.4  
    57.5  header {* List prefixes and postfixes *}
    57.6  
    57.7 -theory List_Prefix = Main:
    57.8 +theory List_Prefix
    57.9 +import Main
   57.10 +begin
   57.11  
   57.12  subsection {* Prefix order on lists *}
   57.13  
    58.1 --- a/src/HOL/Library/Multiset.thy	Mon Aug 16 14:21:54 2004 +0200
    58.2 +++ b/src/HOL/Library/Multiset.thy	Mon Aug 16 14:22:27 2004 +0200
    58.3 @@ -5,7 +5,9 @@
    58.4  
    58.5  header {* Multisets *}
    58.6  
    58.7 -theory Multiset = Accessible_Part:
    58.8 +theory Multiset
    58.9 +import Accessible_Part
   58.10 +begin
   58.11  
   58.12  subsection {* The type of multisets *}
   58.13  
    59.1 --- a/src/HOL/Library/NatPair.thy	Mon Aug 16 14:21:54 2004 +0200
    59.2 +++ b/src/HOL/Library/NatPair.thy	Mon Aug 16 14:22:27 2004 +0200
    59.3 @@ -6,7 +6,9 @@
    59.4  
    59.5  header {* Pairs of Natural Numbers *}
    59.6  
    59.7 -theory NatPair = Main:
    59.8 +theory NatPair
    59.9 +import Main
   59.10 +begin
   59.11  
   59.12  text{*
   59.13    An injective function from @{text "\<nat>\<twosuperior>"} to @{text
    60.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Aug 16 14:21:54 2004 +0200
    60.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 16 14:22:27 2004 +0200
    60.3 @@ -5,7 +5,9 @@
    60.4  
    60.5  header {* Natural numbers with infinity *}
    60.6  
    60.7 -theory Nat_Infinity = Main:
    60.8 +theory Nat_Infinity
    60.9 +import Main
   60.10 +begin
   60.11  
   60.12  subsection "Definitions"
   60.13  
    61.1 --- a/src/HOL/Library/Nested_Environment.thy	Mon Aug 16 14:21:54 2004 +0200
    61.2 +++ b/src/HOL/Library/Nested_Environment.thy	Mon Aug 16 14:22:27 2004 +0200
    61.3 @@ -5,7 +5,9 @@
    61.4  
    61.5  header {* Nested environments *}
    61.6  
    61.7 -theory Nested_Environment = Main:
    61.8 +theory Nested_Environment
    61.9 +import Main
   61.10 +begin
   61.11  
   61.12  text {*
   61.13    Consider a partial function @{term [source] "e :: 'a => 'b option"};
    62.1 --- a/src/HOL/Library/Permutation.thy	Mon Aug 16 14:21:54 2004 +0200
    62.2 +++ b/src/HOL/Library/Permutation.thy	Mon Aug 16 14:22:27 2004 +0200
    62.3 @@ -4,7 +4,9 @@
    62.4  
    62.5  header {* Permutations *}
    62.6  
    62.7 -theory Permutation = Multiset:
    62.8 +theory Permutation
    62.9 +import Multiset
   62.10 +begin
   62.11  
   62.12  consts
   62.13    perm :: "('a list * 'a list) set"
    63.1 --- a/src/HOL/Library/Primes.thy	Mon Aug 16 14:21:54 2004 +0200
    63.2 +++ b/src/HOL/Library/Primes.thy	Mon Aug 16 14:22:27 2004 +0200
    63.3 @@ -6,7 +6,9 @@
    63.4  
    63.5  header {* The Greatest Common Divisor and Euclid's algorithm *}
    63.6  
    63.7 -theory Primes = Main:
    63.8 +theory Primes
    63.9 +import Main
   63.10 +begin
   63.11  
   63.12  text {*
   63.13    See \cite{davenport92}.
    64.1 --- a/src/HOL/Library/Quotient.thy	Mon Aug 16 14:21:54 2004 +0200
    64.2 +++ b/src/HOL/Library/Quotient.thy	Mon Aug 16 14:22:27 2004 +0200
    64.3 @@ -5,7 +5,9 @@
    64.4  
    64.5  header {* Quotient types *}
    64.6  
    64.7 -theory Quotient = Main:
    64.8 +theory Quotient
    64.9 +import Main
   64.10 +begin
   64.11  
   64.12  text {*
   64.13   We introduce the notion of quotient types over equivalence relations
    65.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Aug 16 14:21:54 2004 +0200
    65.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Aug 16 14:22:27 2004 +0200
    65.3 @@ -6,7 +6,9 @@
    65.4  
    65.5  header {* A general ``while'' combinator *}
    65.6  
    65.7 -theory While_Combinator = Main:
    65.8 +theory While_Combinator
    65.9 +import Main
   65.10 +begin
   65.11  
   65.12  text {*
   65.13   We define a while-combinator @{term while} and prove: (a) an
    66.1 --- a/src/HOL/Library/Word.thy	Mon Aug 16 14:21:54 2004 +0200
    66.2 +++ b/src/HOL/Library/Word.thy	Mon Aug 16 14:22:27 2004 +0200
    66.3 @@ -5,7 +5,10 @@
    66.4  
    66.5  header {* Binary Words *}
    66.6  
    66.7 -theory Word = Main files "word_setup.ML":
    66.8 +theory Word
    66.9 +import Main
   66.10 +files "word_setup.ML"
   66.11 +begin
   66.12  
   66.13  subsection {* Auxilary Lemmas *}
   66.14  
    67.1 --- a/src/HOL/Library/Zorn.thy	Mon Aug 16 14:21:54 2004 +0200
    67.2 +++ b/src/HOL/Library/Zorn.thy	Mon Aug 16 14:22:27 2004 +0200
    67.3 @@ -6,7 +6,9 @@
    67.4  
    67.5  header {* Zorn's Lemma *}
    67.6  
    67.7 -theory Zorn = Main:
    67.8 +theory Zorn
    67.9 +import Main
   67.10 +begin
   67.11  
   67.12  text{*
   67.13    The lemma and section numbers refer to an unpublished article
    68.1 --- a/src/HOL/List.thy	Mon Aug 16 14:21:54 2004 +0200
    68.2 +++ b/src/HOL/List.thy	Mon Aug 16 14:22:27 2004 +0200
    68.3 @@ -5,7 +5,9 @@
    68.4  
    68.5  header {* The datatype of finite lists *}
    68.6  
    68.7 -theory List = PreList:
    68.8 +theory List
    68.9 +import PreList
   68.10 +begin
   68.11  
   68.12  datatype 'a list =
   68.13      Nil    ("[]")
    69.1 --- a/src/HOL/Main.thy	Mon Aug 16 14:21:54 2004 +0200
    69.2 +++ b/src/HOL/Main.thy	Mon Aug 16 14:22:27 2004 +0200
    69.3 @@ -5,7 +5,9 @@
    69.4  
    69.5  header {* Main HOL *}
    69.6  
    69.7 -theory Main = Map + Infinite_Set + Extraction + Refute:
    69.8 +theory Main
    69.9 +import Map Infinite_Set Extraction Refute
   69.10 +begin
   69.11  
   69.12  text {*
   69.13    Theory @{text Main} includes everything.  Note that theory @{text
    70.1 --- a/src/HOL/Map.thy	Mon Aug 16 14:21:54 2004 +0200
    70.2 +++ b/src/HOL/Map.thy	Mon Aug 16 14:22:27 2004 +0200
    70.3 @@ -8,7 +8,9 @@
    70.4  
    70.5  header {* Maps *}
    70.6  
    70.7 -theory Map = List:
    70.8 +theory Map
    70.9 +import List
   70.10 +begin
   70.11  
   70.12  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
   70.13  translations (type) "a ~=> b " <= (type) "a => b option"
    71.1 --- a/src/HOL/Nat.thy	Mon Aug 16 14:21:54 2004 +0200
    71.2 +++ b/src/HOL/Nat.thy	Mon Aug 16 14:22:27 2004 +0200
    71.3 @@ -8,7 +8,9 @@
    71.4  
    71.5  header {* Natural numbers *}
    71.6  
    71.7 -theory Nat = Wellfounded_Recursion + Ring_and_Field:
    71.8 +theory Nat
    71.9 +import Wellfounded_Recursion Ring_and_Field
   71.10 +begin
   71.11  
   71.12  subsection {* Type @{text ind} *}
   71.13  
    72.1 --- a/src/HOL/NatArith.thy	Mon Aug 16 14:21:54 2004 +0200
    72.2 +++ b/src/HOL/NatArith.thy	Mon Aug 16 14:22:27 2004 +0200
    72.3 @@ -5,8 +5,10 @@
    72.4  
    72.5  header {* More arithmetic on natural numbers *}
    72.6  
    72.7 -theory NatArith = Nat
    72.8 -files "arith_data.ML":
    72.9 +theory NatArith
   72.10 +import Nat
   72.11 +files "arith_data.ML"
   72.12 +begin
   72.13  
   72.14  setup arith_setup
   72.15  
    73.1 --- a/src/HOL/OrderedGroup.thy	Mon Aug 16 14:21:54 2004 +0200
    73.2 +++ b/src/HOL/OrderedGroup.thy	Mon Aug 16 14:22:27 2004 +0200
    73.3 @@ -5,8 +5,10 @@
    73.4  
    73.5  header {* Ordered Groups *}
    73.6  
    73.7 -theory OrderedGroup = Inductive + LOrder
    73.8 -  files "../Provers/Arith/abel_cancel.ML":
    73.9 +theory OrderedGroup
   73.10 +import Inductive LOrder
   73.11 +files "../Provers/Arith/abel_cancel.ML"
   73.12 +begin
   73.13  
   73.14  text {*
   73.15    The theory of partially ordered groups is taken from the books:
    74.1 --- a/src/HOL/Power.thy	Mon Aug 16 14:21:54 2004 +0200
    74.2 +++ b/src/HOL/Power.thy	Mon Aug 16 14:22:27 2004 +0200
    74.3 @@ -7,7 +7,9 @@
    74.4  
    74.5  header{*Exponentiation and Binomial Coefficients*}
    74.6  
    74.7 -theory Power = Divides:
    74.8 +theory Power
    74.9 +import Divides
   74.10 +begin
   74.11  
   74.12  subsection{*Powers for Arbitrary Semirings*}
   74.13  
    75.1 --- a/src/HOL/PreList.thy	Mon Aug 16 14:21:54 2004 +0200
    75.2 +++ b/src/HOL/PreList.thy	Mon Aug 16 14:22:27 2004 +0200
    75.3 @@ -6,8 +6,9 @@
    75.4  
    75.5  header{*A Basis for Building the Theory of Lists*}
    75.6  
    75.7 -theory PreList =
    75.8 -    Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
    75.9 +theory PreList
   75.10 +import Wellfounded_Relations Presburger Recdef Relation_Power Parity
   75.11 +begin
   75.12  
   75.13  text {*
   75.14    Is defined separately to serve as a basis for theory ToyList in the
    76.1 --- a/src/HOL/Presburger.thy	Mon Aug 16 14:21:54 2004 +0200
    76.2 +++ b/src/HOL/Presburger.thy	Mon Aug 16 14:22:27 2004 +0200
    76.3 @@ -6,14 +6,12 @@
    76.4  generation for Cooper Algorithm  
    76.5  *)
    76.6  
    76.7 -header {* Presburger Arithmetic: Cooper Algorithm *}
    76.8 +header {* Presburger Arithmetic: Cooper's Algorithm *}
    76.9  
   76.10 -theory Presburger = NatSimprocs + SetInterval
   76.11 -files
   76.12 -  ("cooper_dec.ML")
   76.13 -  ("cooper_proof.ML")
   76.14 -  ("qelim.ML")
   76.15 -  ("presburger.ML"):
   76.16 +theory Presburger
   76.17 +import NatSimprocs SetInterval
   76.18 +files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
   76.19 +begin
   76.20  
   76.21  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
   76.22  
    77.1 --- a/src/HOL/Product_Type.thy	Mon Aug 16 14:21:54 2004 +0200
    77.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 16 14:22:27 2004 +0200
    77.3 @@ -6,8 +6,10 @@
    77.4  
    77.5  header {* Cartesian products *}
    77.6  
    77.7 -theory Product_Type = Fun
    77.8 -files ("Tools/split_rule.ML"):
    77.9 +theory Product_Type
   77.10 +import Fun
   77.11 +files ("Tools/split_rule.ML")
   77.12 +begin
   77.13  
   77.14  subsection {* Unit *}
   77.15  
    78.1 --- a/src/HOL/Real/Lubs.thy	Mon Aug 16 14:21:54 2004 +0200
    78.2 +++ b/src/HOL/Real/Lubs.thy	Mon Aug 16 14:22:27 2004 +0200
    78.3 @@ -6,7 +6,9 @@
    78.4  
    78.5  header{*Definitions of Upper Bounds and Least Upper Bounds*}
    78.6  
    78.7 -theory Lubs = Main:
    78.8 +theory Lubs
    78.9 +import Main
   78.10 +begin
   78.11  
   78.12  text{*Thanks to suggestions by James Margetson*}
   78.13  
    79.1 --- a/src/HOL/Real/PReal.thy	Mon Aug 16 14:21:54 2004 +0200
    79.2 +++ b/src/HOL/Real/PReal.thy	Mon Aug 16 14:22:27 2004 +0200
    79.3 @@ -7,7 +7,9 @@
    79.4                    provides some of the definitions.
    79.5  *)
    79.6  
    79.7 -theory PReal = Rational:
    79.8 +theory PReal
    79.9 +import Rational
   79.10 +begin
   79.11  
   79.12  text{*Could be generalized and moved to @{text Ring_and_Field}*}
   79.13  lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
    80.1 --- a/src/HOL/Real/RComplete.thy	Mon Aug 16 14:21:54 2004 +0200
    80.2 +++ b/src/HOL/Real/RComplete.thy	Mon Aug 16 14:22:27 2004 +0200
    80.3 @@ -8,7 +8,9 @@
    80.4  
    80.5  header{*Completeness of the Reals; Floor and Ceiling Functions*}
    80.6  
    80.7 -theory RComplete = Lubs + RealDef:
    80.8 +theory RComplete
    80.9 +import Lubs RealDef
   80.10 +begin
   80.11  
   80.12  lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
   80.13  by simp
    81.1 --- a/src/HOL/Real/Rational.thy	Mon Aug 16 14:21:54 2004 +0200
    81.2 +++ b/src/HOL/Real/Rational.thy	Mon Aug 16 14:22:27 2004 +0200
    81.3 @@ -5,8 +5,10 @@
    81.4  
    81.5  header {* Rational numbers *}
    81.6  
    81.7 -theory Rational = Quotient + Main
    81.8 -files ("rat_arith.ML"):
    81.9 +theory Rational
   81.10 +import Quotient
   81.11 +files ("rat_arith.ML")
   81.12 +begin
   81.13  
   81.14  subsection {* Fractions *}
   81.15  
    82.1 --- a/src/HOL/Real/RealDef.thy	Mon Aug 16 14:21:54 2004 +0200
    82.2 +++ b/src/HOL/Real/RealDef.thy	Mon Aug 16 14:22:27 2004 +0200
    82.3 @@ -7,8 +7,10 @@
    82.4  
    82.5  header{*Defining the Reals from the Positive Reals*}
    82.6  
    82.7 -theory RealDef = PReal
    82.8 -files ("real_arith.ML"):
    82.9 +theory RealDef
   82.10 +import PReal
   82.11 +files ("real_arith.ML")
   82.12 +begin
   82.13  
   82.14  constdefs
   82.15    realrel   ::  "((preal * preal) * (preal * preal)) set"
    83.1 --- a/src/HOL/Real/RealPow.thy	Mon Aug 16 14:21:54 2004 +0200
    83.2 +++ b/src/HOL/Real/RealPow.thy	Mon Aug 16 14:22:27 2004 +0200
    83.3 @@ -6,7 +6,9 @@
    83.4  
    83.5  *)
    83.6  
    83.7 -theory RealPow = RealDef:
    83.8 +theory RealPow
    83.9 +import RealDef
   83.10 +begin
   83.11  
   83.12  declare abs_mult_self [simp]
   83.13  
    84.1 --- a/src/HOL/Recdef.thy	Mon Aug 16 14:21:54 2004 +0200
    84.2 +++ b/src/HOL/Recdef.thy	Mon Aug 16 14:22:27 2004 +0200
    84.3 @@ -5,7 +5,8 @@
    84.4  
    84.5  header {* TFL: recursive function definitions *}
    84.6  
    84.7 -theory Recdef = Wellfounded_Relations + Datatype
    84.8 +theory Recdef
    84.9 +import Wellfounded_Relations Datatype
   84.10  files
   84.11    ("../TFL/utils.ML")
   84.12    ("../TFL/usyntax.ML")
   84.13 @@ -15,7 +16,8 @@
   84.14    ("../TFL/thry.ML")
   84.15    ("../TFL/tfl.ML")
   84.16    ("../TFL/post.ML")
   84.17 -  ("Tools/recdef_package.ML"):
   84.18 +  ("Tools/recdef_package.ML")
   84.19 +begin
   84.20  
   84.21  lemma tfl_eq_True: "(x = True) --> x"
   84.22    by blast
    85.1 --- a/src/HOL/Record.thy	Mon Aug 16 14:21:54 2004 +0200
    85.2 +++ b/src/HOL/Record.thy	Mon Aug 16 14:22:27 2004 +0200
    85.3 @@ -3,8 +3,10 @@
    85.4      Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
    85.5  *)
    85.6  
    85.7 -theory Record = Product_Type
    85.8 -files ("Tools/record_package.ML"):
    85.9 +theory Record
   85.10 +import Product_Type
   85.11 +files ("Tools/record_package.ML")
   85.12 +begin
   85.13  
   85.14  ML {*
   85.15  val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
    86.1 --- a/src/HOL/Refute.thy	Mon Aug 16 14:21:54 2004 +0200
    86.2 +++ b/src/HOL/Refute.thy	Mon Aug 16 14:22:27 2004 +0200
    86.3 @@ -8,12 +8,13 @@
    86.4  
    86.5  header {* Refute *}
    86.6  
    86.7 -theory Refute = Map
    86.8 -
    86.9 +theory Refute
   86.10 +import Map
   86.11  files "Tools/prop_logic.ML"
   86.12        "Tools/sat_solver.ML"
   86.13        "Tools/refute.ML"
   86.14 -      "Tools/refute_isar.ML":
   86.15 +      "Tools/refute_isar.ML"
   86.16 +begin
   86.17  
   86.18  setup Refute.setup
   86.19  
    87.1 --- a/src/HOL/Relation.thy	Mon Aug 16 14:21:54 2004 +0200
    87.2 +++ b/src/HOL/Relation.thy	Mon Aug 16 14:22:27 2004 +0200
    87.3 @@ -6,7 +6,9 @@
    87.4  
    87.5  header {* Relations *}
    87.6  
    87.7 -theory Relation = Product_Type:
    87.8 +theory Relation
    87.9 +import Product_Type
   87.10 +begin
   87.11  
   87.12  subsection {* Definitions *}
   87.13  
    88.1 --- a/src/HOL/Relation_Power.thy	Mon Aug 16 14:21:54 2004 +0200
    88.2 +++ b/src/HOL/Relation_Power.thy	Mon Aug 16 14:22:27 2004 +0200
    88.3 @@ -12,7 +12,9 @@
    88.4  Examples: range(f^n) = A and Range(R^n) = B need constraints.
    88.5  *)
    88.6  
    88.7 -theory Relation_Power = Nat:
    88.8 +theory Relation_Power
    88.9 +import Nat
   88.10 +begin
   88.11  
   88.12  instance
   88.13    set :: (type) power ..  (* only ('a * 'a) set should be in power! *)
    89.1 --- a/src/HOL/Ring_and_Field.thy	Mon Aug 16 14:21:54 2004 +0200
    89.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Aug 16 14:22:27 2004 +0200
    89.3 @@ -5,7 +5,9 @@
    89.4  
    89.5  header {* (Ordered) Rings and Fields *}
    89.6  
    89.7 -theory Ring_and_Field = OrderedGroup:
    89.8 +theory Ring_and_Field 
    89.9 +import OrderedGroup
   89.10 +begin
   89.11  
   89.12  text {*
   89.13    The theory of partially ordered rings is taken from the books:
    90.1 --- a/src/HOL/Set.thy	Mon Aug 16 14:21:54 2004 +0200
    90.2 +++ b/src/HOL/Set.thy	Mon Aug 16 14:22:27 2004 +0200
    90.3 @@ -5,7 +5,9 @@
    90.4  
    90.5  header {* Set theory for higher-order logic *}
    90.6  
    90.7 -theory Set = HOL:
    90.8 +theory Set
    90.9 +import HOL
   90.10 +begin
   90.11  
   90.12  text {* A set in HOL is simply a predicate. *}
   90.13  
    91.1 --- a/src/HOL/SetInterval.thy	Mon Aug 16 14:21:54 2004 +0200
    91.2 +++ b/src/HOL/SetInterval.thy	Mon Aug 16 14:22:27 2004 +0200
    91.3 @@ -9,7 +9,9 @@
    91.4  
    91.5  header {* Set intervals *}
    91.6  
    91.7 -theory SetInterval = IntArith:
    91.8 +theory SetInterval
    91.9 +import IntArith
   91.10 +begin
   91.11  
   91.12  constdefs
   91.13    lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")
    92.1 --- a/src/HOL/Transitive_Closure.thy	Mon Aug 16 14:21:54 2004 +0200
    92.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Aug 16 14:22:27 2004 +0200
    92.3 @@ -6,9 +6,10 @@
    92.4  
    92.5  header {* Reflexive and Transitive closure of a relation *}
    92.6  
    92.7 -theory Transitive_Closure = Inductive
    92.8 -
    92.9 -files ("../Provers/trancl.ML"):
   92.10 +theory Transitive_Closure
   92.11 +import Inductive
   92.12 +files ("../Provers/trancl.ML")
   92.13 +begin
   92.14  
   92.15  text {*
   92.16    @{text rtrancl} is reflexive/transitive closure,
    93.1 --- a/src/HOL/Typedef.thy	Mon Aug 16 14:21:54 2004 +0200
    93.2 +++ b/src/HOL/Typedef.thy	Mon Aug 16 14:22:27 2004 +0200
    93.3 @@ -5,8 +5,10 @@
    93.4  
    93.5  header {* HOL type definitions *}
    93.6  
    93.7 -theory Typedef = Set
    93.8 -files ("Tools/typedef_package.ML"):
    93.9 +theory Typedef
   93.10 +import Set
   93.11 +files ("Tools/typedef_package.ML")
   93.12 +begin
   93.13  
   93.14  locale type_definition =
   93.15    fixes Rep and Abs and A