New theory header syntax.

--- a/src/HOL/Complex/CLim.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/CLim.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Limits, Continuity and Differentiation for Complex Functions*}
 
-theory CLim = CSeries:
+theory CLim
+import CSeries
+begin
 
 (*not in simpset?*)
 declare hypreal_epsilon_not_zero [simp]

--- a/src/HOL/Complex/CSeries.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/CSeries.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header{*Finite Summation and Infinite Series for Complex Numbers*}
 
-theory CSeries = CStar:
+theory CSeries
+import CStar
+begin
 
 consts sumc :: "[nat,nat,(nat=>complex)] => complex"
 primrec

--- a/src/HOL/Complex/CStar.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/CStar.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 header{*Star-transforms in NSA, Extending Sets of Complex Numbers
       and Complex Functions*}
 
-theory CStar = NSCA:
+theory CStar
+import NSCA
+begin
 
 constdefs
 

--- a/src/HOL/Complex/Complex.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header {* Complex Numbers: Rectangular and Polar Representations *}
 
-theory Complex = "../Hyperreal/HLog":
+theory Complex
+import "../Hyperreal/HLog"
+begin
 
 datatype complex = Complex real real
 

--- a/src/HOL/Complex/ComplexBin.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/ComplexBin.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,5 +5,9 @@
                 This case is reduced to that for the reals.
 *)
 
-theory ComplexBin = Complex:
+theory ComplexBin
+import Complex
+begin
 
+end
+

--- a/src/HOL/Complex/Complex_Main.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/Complex_Main.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,6 +6,8 @@
 
 header{*Comprehensive Complex Theory*}
 
-theory Complex_Main = CLim:
+theory Complex_Main
+import CLim
+begin
 
 end

--- a/src/HOL/Complex/NSCA.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/NSCA.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header{*Non-Standard Complex Analysis*}
 
-theory NSCA = NSComplex:
+theory NSCA
+import NSComplex
+begin
 
 constdefs
 

--- a/src/HOL/Complex/NSComplex.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Nonstandard Complex Numbers*}
 
-theory NSComplex = Complex:
+theory NSComplex
+import Complex
+begin
 
 constdefs
     hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"

--- a/src/HOL/Datatype.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Datatype.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Datatypes *}
 
-theory Datatype = Datatype_Universe:
+theory Datatype
+import Datatype_Universe
+begin
 
 subsection {* Representing primitive types *}
 

--- a/src/HOL/Divides.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Divides.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 The division operators div, mod and the divides relation "dvd"
 *)
 
-theory Divides = NatArith:
+theory Divides
+import NatArith
+begin
 
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)

--- a/src/HOL/Extraction.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Extraction.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,9 +5,10 @@
 
 header {* Program extraction for HOL *}
 
-theory Extraction = Datatype
-files
-  "Tools/rewrite_hol_proof.ML":
+theory Extraction
+import Datatype
+files "Tools/rewrite_hol_proof.ML"
+begin
 
 subsection {* Setup *}
 

--- a/src/HOL/Finite_Set.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Finite sets *}
 
-theory Finite_Set = Divides + Power + Inductive:
+theory Finite_Set
+import Divides Power Inductive
+begin
 
 subsection {* Collection of finite sets *}
 

--- a/src/HOL/Fun.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Fun.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 Notions about functions.
 *)
 
-theory Fun = Typedef:
+theory Fun 
+import Typedef
+begin
 
 instance set :: (type) order
   by (intro_classes,

--- a/src/HOL/Gfp.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Gfp.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 Greatest fixed points (requires Lfp too!)
 *)
 
-theory Gfp = Lfp:
+theory Gfp 
+import Lfp
+begin
 
 constdefs
   gfp :: "['a set=>'a set] => 'a set"

--- a/src/HOL/HOL.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,9 +5,10 @@
 
 header {* The basis of Higher-Order Logic *}
 
-theory HOL = CPure
-files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
-
+theory HOL
+import CPure
+files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+begin
 
 subsection {* Primitive logic *}
 

--- a/src/HOL/Hilbert_Choice.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,9 +6,10 @@
 
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
-theory Hilbert_Choice = NatArith
-files ("Tools/meson.ML") ("Tools/specification_package.ML"):
-
+theory Hilbert_Choice
+import NatArith
+files ("Tools/meson.ML") ("Tools/specification_package.ML")
+begin
 
 subsection {* Hilbert's epsilon *}
 

--- a/src/HOL/Hyperreal/EvenOdd.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Even and Odd Numbers: Compatibility file for Parity*}
 
-theory EvenOdd = NthRoot:
+theory EvenOdd
+import NthRoot
+begin
 
 subsection{*General Lemmas About Division*}
 

--- a/src/HOL/Hyperreal/Fact.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Factorial Function*}
 
-theory Fact = Real:
+theory Fact
+import Real
+begin
 
 consts fact :: "nat => nat"
 primrec
@@ -71,4 +73,4 @@
 by (case_tac "m", auto)
 
 
-end
\ No newline at end of file
+end

--- a/src/HOL/Hyperreal/Filter.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Filter.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Filters and Ultrafilters*}
 
-theory Filter = Zorn:
+theory Filter
+import Zorn
+begin
 
 constdefs
 

--- a/src/HOL/Hyperreal/HLog.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header{*Logarithms: Non-Standard Version*}
 
-theory HLog = Log + HTranscendental: 
+theory HLog
+import Log HTranscendental
+begin
 
 
 (* should be in NSA.ML *)

--- a/src/HOL/Hyperreal/HSeries.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Finite Summation and Infinite Series for Hyperreals*}
 
-theory HSeries = Series:
+theory HSeries
+import Series
+begin
 
 constdefs 
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"

--- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Nonstandard Extensions of Transcendental Functions*}
 
-theory HTranscendental = Transcendental + Integration:
+theory HTranscendental
+import Transcendental Integration
+begin
 
 text{*really belongs in Transcendental*}
 lemma sqrt_divide_self_eq:

--- a/src/HOL/Hyperreal/HyperArith.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,9 +6,10 @@
 
 header{*Binary arithmetic and Simplification for the Hyperreals*}
 
-theory HyperArith = HyperDef
-files ("hypreal_arith.ML"):
-
+theory HyperArith
+import HyperDef
+files ("hypreal_arith.ML")
+begin
 
 subsection{*Numerals and Arithmetic*}
 

--- a/src/HOL/Hyperreal/HyperDef.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,9 +7,10 @@
 
 header{*Construction of Hyperreals Using Ultrafilters*}
 
-theory HyperDef = Filter + "../Real/Real"
-files ("fuf.ML"):  (*Warning: file fuf.ML refers to the name Hyperdef!*)
-
+theory HyperDef
+import Filter "../Real/Real"
+files ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
+begin
 
 constdefs
 

--- a/src/HOL/Hyperreal/HyperNat.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Construction of Hypernaturals using Ultrafilters*}
 
-theory HyperNat = Star:
+theory HyperNat
+import Star
+begin
 
 constdefs
     hypnatrel :: "((nat=>nat)*(nat=>nat)) set"

--- a/src/HOL/Hyperreal/HyperPow.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Exponentials on the Hyperreals*}
 
-theory HyperPow = HyperArith + HyperNat + "../Real/RealPow":
+theory HyperPow
+import HyperArith HyperNat "../Real/RealPow"
+begin
 
 instance hypreal :: power ..
 

--- a/src/HOL/Hyperreal/Hyperreal.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Hyperreal.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,6 +7,8 @@
 and mechanization of Nonstandard Real Analysis
 *)
 
-theory Hyperreal = Poly + MacLaurin + HLog:
+theory Hyperreal
+import Poly MacLaurin HLog
+begin
 
 end

--- a/src/HOL/Hyperreal/Integration.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Theory of Integration*}
 
-theory Integration = MacLaurin:
+theory Integration
+import MacLaurin
+begin
 
 text{*We follow John Harrison in formalizing the Gauge integral.*}
 

--- a/src/HOL/Hyperreal/Lim.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Limits, Continuity and Differentiation*}
 
-theory Lim = SEQ + RealDef:
+theory Lim
+import SEQ RealDef
+begin
 
 text{*Standard and Nonstandard Definitions*}
 

--- a/src/HOL/Hyperreal/Log.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Log.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header{*Logarithms: Standard Version*}
 
-theory Log = Transcendental:
+theory Log
+import Transcendental
+begin
 
 constdefs
 

--- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-theory MacLaurin = Log:
+theory MacLaurin
+import Log
+begin
 
 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
 by (induct_tac "n", auto)

--- a/src/HOL/Hyperreal/NSA.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
-theory NSA = HyperArith + RComplete:
+theory NSA
+import HyperArith RComplete
+begin
 
 constdefs
 

--- a/src/HOL/Hyperreal/NatStar.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,8 +7,9 @@
 
 header{*Star-transforms for the Hypernaturals*}
 
-theory NatStar = "../Real/RealPow" + HyperPow:
-
+theory NatStar
+import "../Real/RealPow" HyperPow
+begin
 
 text{*Extends sets of nats, and functions from the nats to nats or reals*}
 

--- a/src/HOL/Hyperreal/NthRoot.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Existence of Nth Root*}
 
-theory NthRoot = SEQ + HSeries:
+theory NthRoot
+import SEQ HSeries
+begin
 
 text {*
   Various lemmas needed for this result. We follow the proof given by

--- a/src/HOL/Hyperreal/Poly.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -8,8 +8,9 @@
 
 header{*Univariate Real Polynomials*}
 
-theory Poly = Transcendental:
-
+theory Poly
+import Transcendental
+begin
 
 text{*Application of polynomial as a real function.*}
 

--- a/src/HOL/Hyperreal/SEQ.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-theory SEQ = NatStar + HyperPow:
+theory SEQ
+import NatStar HyperPow
+begin
 
 constdefs
 

--- a/src/HOL/Hyperreal/Series.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Finite Summation and Infinite Series*}
 
-theory Series = SEQ + Lim:
+theory Series
+import SEQ Lim
+begin
 
 syntax sumr :: "[nat,nat,(nat=>real)] => real"
 translations

--- a/src/HOL/Hyperreal/Star.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Star-Transforms in Non-Standard Analysis*}
 
-theory Star = NSA:
+theory Star
+import NSA
+begin
 
 constdefs
     (* nonstandard extension of sets *)

--- a/src/HOL/Hyperreal/Transcendental.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Power Series, Transcendental Functions etc.*}
 
-theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:
+theory Transcendental
+import NthRoot Fact HSeries EvenOdd Lim
+begin
 
 constdefs
     root :: "[nat,real] => real"

--- a/src/HOL/Inductive.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Inductive.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,8 @@
 
 header {* Support for inductive sets and types *}
 
-theory Inductive = Gfp + Sum_Type + Relation + Record
+theory Inductive 
+import Gfp Sum_Type Relation Record
 files
   ("Tools/inductive_package.ML")
   ("Tools/inductive_realizer.ML")
@@ -18,8 +19,8 @@
   ("Tools/datatype_package.ML")
   ("Tools/datatype_codegen.ML")
   ("Tools/recfun_codegen.ML")
-  ("Tools/primrec_package.ML"):
-
+  ("Tools/primrec_package.ML")
+begin
 
 subsection {* Inductive sets *}
 

--- a/src/HOL/Infinite_Set.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Infnite Sets and Related Concepts*}
 
-theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval:
+theory Infinite_Set
+import Hilbert_Choice Finite_Set SetInterval
+begin
 
 subsection "Infinite Sets"
 

--- a/src/HOL/Integ/Equiv.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Equivalence relations in Higher-Order Set Theory *}
 
-theory Equiv = Relation + Finite_Set:
+theory Equiv
+import Relation Finite_Set
+begin
 
 subsection {* Equivalence relations *}
 

--- a/src/HOL/Integ/IntArith.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/IntArith.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,8 +5,10 @@
 
 header {* Integer arithmetic *}
 
-theory IntArith = Numeral
-files ("int_arith1.ML"):
+theory IntArith
+import Numeral
+files ("int_arith1.ML")
+begin
 
 text{*Duplicate: can't understand why it's necessary*}
 declare numeral_0_eq_0 [simp]

--- a/src/HOL/Integ/IntDef.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
 
-theory IntDef = Equiv + NatArith:
+theory IntDef
+import Equiv NatArith
+begin
 
 constdefs
   intrel :: "((nat * nat) * (nat * nat)) set"

--- a/src/HOL/Integ/IntDiv.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -31,8 +31,10 @@
 *)
 
 
-theory IntDiv = IntArith + Recdef
-  files ("IntDiv_setup.ML"):
+theory IntDiv
+import IntArith Recdef
+files ("IntDiv_setup.ML")
+begin
 
 declare zless_nat_conj [simp]
 

--- a/src/HOL/Integ/NatBin.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Binary arithmetic for the natural numbers *}
 
-theory NatBin = IntDiv:
+theory NatBin
+import IntDiv
+begin
 
 text {*
   Arithmetic for naturals is reduced to that for the non-negative integers.

--- a/src/HOL/Integ/NatSimprocs.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,8 +5,10 @@
 
 header {*Simprocs for the Naturals*}
 
-theory NatSimprocs = NatBin
-files "int_factor_simprocs.ML" "nat_simprocs.ML":
+theory NatSimprocs
+import NatBin
+files "int_factor_simprocs.ML" "nat_simprocs.ML"
+begin
 
 setup nat_simprocs_setup
 

--- a/src/HOL/Integ/Numeral.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/Numeral.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,8 +6,10 @@
 
 header{*Arithmetic on Binary Integers*}
 
-theory Numeral = IntDef
-files "Tools/numeral_syntax.ML":
+theory Numeral
+import IntDef
+files "Tools/numeral_syntax.ML"
+begin
 
 text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
    Only qualified access Numeral.Pls and Numeral.Min is allowed.

--- a/src/HOL/Integ/Parity.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/Parity.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Parity: Even and Odd for ints and nats*}
 
-theory Parity = Divides + IntDiv + NatSimprocs:
+theory Parity
+import Divides IntDiv NatSimprocs
+begin
 
 axclass even_odd < type
 

--- a/src/HOL/Integ/Presburger.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,14 +6,12 @@
 generation for Cooper Algorithm  
 *)
 
-header {* Presburger Arithmetic: Cooper Algorithm *}
+header {* Presburger Arithmetic: Cooper's Algorithm *}
 
-theory Presburger = NatSimprocs + SetInterval
-files
-  ("cooper_dec.ML")
-  ("cooper_proof.ML")
-  ("qelim.ML")
-  ("presburger.ML"):
+theory Presburger
+import NatSimprocs SetInterval
+files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
+begin
 
 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
 

--- a/src/HOL/LOrder.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/LOrder.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Lattice Orders *}
 
-theory LOrder = HOL:
+theory LOrder
+import HOL
+begin
 
 text {*
   The theory of lattices developed here is taken from the book:
@@ -327,4 +329,4 @@
 val modular_le = thm "modular_le";
 *}
 
-end
\ No newline at end of file
+end

--- a/src/HOL/Lfp.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Lfp.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 The Knaster-Tarski Theorem
 *)
 
-theory Lfp = Product_Type:
+theory Lfp
+import Product_Type
+begin
 
 constdefs
   lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"

--- a/src/HOL/Library/Accessible_Part.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Accessible_Part.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,8 +6,9 @@
 
 header {* The accessible part of a relation *}
 
-theory Accessible_Part = Main:
-
+theory Accessible_Part
+import Main
+begin
 
 subsection {* Inductive definition *}
 

--- a/src/HOL/Library/Continuity.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Continuity.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Continuity and iterations (of set transformers) *}
 
-theory Continuity = Main:
+theory Continuity
+import Main
+begin
 
 subsection "Chains"
 

--- a/src/HOL/Library/FuncSet.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Pi and Function Sets *}
 
-theory FuncSet = Main:
+theory FuncSet
+import Main
+begin
 
 constdefs
   Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"

--- a/src/HOL/Library/Library.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Library.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -1,18 +1,20 @@
 (*<*)
-theory Library =
-  Accessible_Part +
-  Continuity +
-  FuncSet +
-  List_Prefix +
-  Multiset +
-  NatPair +
-  Nat_Infinity +
-  Nested_Environment +
-  Permutation +
-  Primes +
-  Quotient +
-  While_Combinator +
-  Word +
-  Zorn:
+theory Library
+import
+  Accessible_Part
+  Continuity
+  FuncSet
+  List_Prefix
+  Multiset
+  NatPair
+  Nat_Infinity
+  Nested_Environment
+  Permutation
+  Primes
+  Quotient
+  While_Combinator
+  Word
+  Zorn
+begin
 end
 (*>*)

--- a/src/HOL/Library/List_Prefix.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* List prefixes and postfixes *}
 
-theory List_Prefix = Main:
+theory List_Prefix
+import Main
+begin
 
 subsection {* Prefix order on lists *}
 

--- a/src/HOL/Library/Multiset.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Multisets *}
 
-theory Multiset = Accessible_Part:
+theory Multiset
+import Accessible_Part
+begin
 
 subsection {* The type of multisets *}
 

--- a/src/HOL/Library/NatPair.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/NatPair.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Pairs of Natural Numbers *}
 
-theory NatPair = Main:
+theory NatPair
+import Main
+begin
 
 text{*
   An injective function from @{text "\<nat>\<twosuperior>"} to @{text

--- a/src/HOL/Library/Nat_Infinity.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Natural numbers with infinity *}
 
-theory Nat_Infinity = Main:
+theory Nat_Infinity
+import Main
+begin
 
 subsection "Definitions"
 

--- a/src/HOL/Library/Nested_Environment.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Nested environments *}
 
-theory Nested_Environment = Main:
+theory Nested_Environment
+import Main
+begin
 
 text {*
   Consider a partial function @{term [source] "e :: 'a => 'b option"};

--- a/src/HOL/Library/Permutation.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Permutation.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -4,7 +4,9 @@
 
 header {* Permutations *}
 
-theory Permutation = Multiset:
+theory Permutation
+import Multiset
+begin
 
 consts
   perm :: "('a list * 'a list) set"

--- a/src/HOL/Library/Primes.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Primes.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* The Greatest Common Divisor and Euclid's algorithm *}
 
-theory Primes = Main:
+theory Primes
+import Main
+begin
 
 text {*
   See \cite{davenport92}.

--- a/src/HOL/Library/Quotient.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Quotient.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Quotient types *}
 
-theory Quotient = Main:
+theory Quotient
+import Main
+begin
 
 text {*
  We introduce the notion of quotient types over equivalence relations

--- a/src/HOL/Library/While_Combinator.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* A general ``while'' combinator *}
 
-theory While_Combinator = Main:
+theory While_Combinator
+import Main
+begin
 
 text {*
  We define a while-combinator @{term while} and prove: (a) an

--- a/src/HOL/Library/Word.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Word.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,10 @@
 
 header {* Binary Words *}
 
-theory Word = Main files "word_setup.ML":
+theory Word
+import Main
+files "word_setup.ML"
+begin
 
 subsection {* Auxilary Lemmas *}
 

--- a/src/HOL/Library/Zorn.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Zorn.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Zorn's Lemma *}
 
-theory Zorn = Main:
+theory Zorn
+import Main
+begin
 
 text{*
   The lemma and section numbers refer to an unpublished article

--- a/src/HOL/List.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/List.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* The datatype of finite lists *}
 
-theory List = PreList:
+theory List
+import PreList
+begin
 
 datatype 'a list =
     Nil    ("[]")

--- a/src/HOL/Main.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Main.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Main HOL *}
 
-theory Main = Map + Infinite_Set + Extraction + Refute:
+theory Main
+import Map Infinite_Set Extraction Refute
+begin
 
 text {*
   Theory @{text Main} includes everything.  Note that theory @{text

--- a/src/HOL/Map.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Map.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -8,7 +8,9 @@
 
 header {* Maps *}
 
-theory Map = List:
+theory Map
+import List
+begin
 
 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
 translations (type) "a ~=> b " <= (type) "a => b option"

--- a/src/HOL/Nat.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Nat.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -8,7 +8,9 @@
 
 header {* Natural numbers *}
 
-theory Nat = Wellfounded_Recursion + Ring_and_Field:
+theory Nat
+import Wellfounded_Recursion Ring_and_Field
+begin
 
 subsection {* Type @{text ind} *}
 

--- a/src/HOL/NatArith.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/NatArith.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,8 +5,10 @@
 
 header {* More arithmetic on natural numbers *}
 
-theory NatArith = Nat
-files "arith_data.ML":
+theory NatArith
+import Nat
+files "arith_data.ML"
+begin
 
 setup arith_setup
 

--- a/src/HOL/OrderedGroup.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/OrderedGroup.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,8 +5,10 @@
 
 header {* Ordered Groups *}
 
-theory OrderedGroup = Inductive + LOrder
-  files "../Provers/Arith/abel_cancel.ML":
+theory OrderedGroup
+import Inductive LOrder
+files "../Provers/Arith/abel_cancel.ML"
+begin
 
 text {*
   The theory of partially ordered groups is taken from the books:

--- a/src/HOL/Power.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Power.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
 
 header{*Exponentiation and Binomial Coefficients*}
 
-theory Power = Divides:
+theory Power
+import Divides
+begin
 
 subsection{*Powers for Arbitrary Semirings*}
 

--- a/src/HOL/PreList.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/PreList.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,8 +6,9 @@
 
 header{*A Basis for Building the Theory of Lists*}
 
-theory PreList =
-    Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
+theory PreList
+import Wellfounded_Relations Presburger Recdef Relation_Power Parity
+begin
 
 text {*
   Is defined separately to serve as a basis for theory ToyList in the

--- a/src/HOL/Presburger.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Presburger.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,14 +6,12 @@
 generation for Cooper Algorithm  
 *)
 
-header {* Presburger Arithmetic: Cooper Algorithm *}
+header {* Presburger Arithmetic: Cooper's Algorithm *}
 
-theory Presburger = NatSimprocs + SetInterval
-files
-  ("cooper_dec.ML")
-  ("cooper_proof.ML")
-  ("qelim.ML")
-  ("presburger.ML"):
+theory Presburger
+import NatSimprocs SetInterval
+files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
+begin
 
 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
 

--- a/src/HOL/Product_Type.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Product_Type.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,8 +6,10 @@
 
 header {* Cartesian products *}
 
-theory Product_Type = Fun
-files ("Tools/split_rule.ML"):
+theory Product_Type
+import Fun
+files ("Tools/split_rule.ML")
+begin
 
 subsection {* Unit *}
 

--- a/src/HOL/Real/Lubs.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/Lubs.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Definitions of Upper Bounds and Least Upper Bounds*}
 
-theory Lubs = Main:
+theory Lubs
+import Main
+begin
 
 text{*Thanks to suggestions by James Margetson*}
 

--- a/src/HOL/Real/PReal.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
                   provides some of the definitions.
 *)
 
-theory PReal = Rational:
+theory PReal
+import Rational
+begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}
 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"

--- a/src/HOL/Real/RComplete.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/RComplete.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -8,7 +8,9 @@
 
 header{*Completeness of the Reals; Floor and Ceiling Functions*}
 
-theory RComplete = Lubs + RealDef:
+theory RComplete
+import Lubs RealDef
+begin
 
 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
 by simp

--- a/src/HOL/Real/Rational.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/Rational.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,8 +5,10 @@
 
 header {* Rational numbers *}
 
-theory Rational = Quotient + Main
-files ("rat_arith.ML"):
+theory Rational
+import Quotient
+files ("rat_arith.ML")
+begin
 
 subsection {* Fractions *}
 

--- a/src/HOL/Real/RealDef.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,8 +7,10 @@
 
 header{*Defining the Reals from the Positive Reals*}
 
-theory RealDef = PReal
-files ("real_arith.ML"):
+theory RealDef
+import PReal
+files ("real_arith.ML")
+begin
 
 constdefs
   realrel   ::  "((preal * preal) * (preal * preal)) set"

--- a/src/HOL/Real/RealPow.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/RealPow.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 *)
 
-theory RealPow = RealDef:
+theory RealPow
+import RealDef
+begin
 
 declare abs_mult_self [simp]
 

--- a/src/HOL/Recdef.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Recdef.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,8 @@
 
 header {* TFL: recursive function definitions *}
 
-theory Recdef = Wellfounded_Relations + Datatype
+theory Recdef
+import Wellfounded_Relations Datatype
 files
   ("../TFL/utils.ML")
   ("../TFL/usyntax.ML")
@@ -15,7 +16,8 @@
   ("../TFL/thry.ML")
   ("../TFL/tfl.ML")
   ("../TFL/post.ML")
-  ("Tools/recdef_package.ML"):
+  ("Tools/recdef_package.ML")
+begin
 
 lemma tfl_eq_True: "(x = True) --> x"
   by blast

--- a/src/HOL/Record.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Record.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -3,8 +3,10 @@
     Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
 *)
 
-theory Record = Product_Type
-files ("Tools/record_package.ML"):
+theory Record
+import Product_Type
+files ("Tools/record_package.ML")
+begin
 
 ML {*
 val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";

--- a/src/HOL/Refute.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Refute.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -8,12 +8,13 @@
 
 header {* Refute *}
 
-theory Refute = Map
-
+theory Refute
+import Map
 files "Tools/prop_logic.ML"
       "Tools/sat_solver.ML"
       "Tools/refute.ML"
-      "Tools/refute_isar.ML":
+      "Tools/refute_isar.ML"
+begin
 
 setup Refute.setup
 

--- a/src/HOL/Relation.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Relation.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Relations *}
 
-theory Relation = Product_Type:
+theory Relation
+import Product_Type
+begin
 
 subsection {* Definitions *}
 

--- a/src/HOL/Relation_Power.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Relation_Power.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -12,7 +12,9 @@
 Examples: range(f^n) = A and Range(R^n) = B need constraints.
 *)
 
-theory Relation_Power = Nat:
+theory Relation_Power
+import Nat
+begin
 
 instance
   set :: (type) power ..  (* only ('a * 'a) set should be in power! *)

--- a/src/HOL/Ring_and_Field.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* (Ordered) Rings and Fields *}
 
-theory Ring_and_Field = OrderedGroup:
+theory Ring_and_Field 
+import OrderedGroup
+begin
 
 text {*
   The theory of partially ordered rings is taken from the books:

--- a/src/HOL/Set.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Set.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Set theory for higher-order logic *}
 
-theory Set = HOL:
+theory Set
+import HOL
+begin
 
 text {* A set in HOL is simply a predicate. *}
 

--- a/src/HOL/SetInterval.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/SetInterval.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -9,7 +9,9 @@
 
 header {* Set intervals *}
 
-theory SetInterval = IntArith:
+theory SetInterval
+import IntArith
+begin
 
 constdefs
   lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")

--- a/src/HOL/Transitive_Closure.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,9 +6,10 @@
 
 header {* Reflexive and Transitive closure of a relation *}
 
-theory Transitive_Closure = Inductive
-
-files ("../Provers/trancl.ML"):
+theory Transitive_Closure
+import Inductive
+files ("../Provers/trancl.ML")
+begin
 
 text {*
   @{text rtrancl} is reflexive/transitive closure,

--- a/src/HOL/Typedef.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Typedef.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,8 +5,10 @@
 
 header {* HOL type definitions *}
 
-theory Typedef = Set
-files ("Tools/typedef_package.ML"):
+theory Typedef
+import Set
+files ("Tools/typedef_package.ML")
+begin
 
 locale type_definition =
   fixes Rep and Abs and A