--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Brackin.thy Fri Jun 17 16:12:49 2005 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-theory Brackin = Main:
+theory Brackin imports Main begin
(* ------------------------------------------------------------------------- *)
(* A couple from Steve Brackin's work. *)
--- a/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Jun 17 16:12:49 2005 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-theory Instructions = Main:
+theory Instructions imports Main begin
(* ------------------------------------------------------------------------- *)
(* Example from Konrad: 68000 instruction set. *)
--- a/Admin/Benchmarks/HOL-datatype/SML.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/Admin/Benchmarks/HOL-datatype/SML.thy Fri Jun 17 16:12:49 2005 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-theory SML = Main:
+theory SML imports Main begin
(* ------------------------------------------------------------------------- *)
(* Example from Myra: part of the syntax of SML. *)
--- a/Admin/Benchmarks/HOL-datatype/Verilog.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Verilog.thy Fri Jun 17 16:12:49 2005 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-theory Verilog = Main:
+theory Verilog imports Main begin
(* ------------------------------------------------------------------------- *)
(* Example from Daryl: a Verilog grammar. *)
--- a/Admin/isa-migrate Fri Jun 17 11:35:35 2005 +0200
+++ b/Admin/isa-migrate Fri Jun 17 16:12:49 2005 +0200
@@ -23,8 +23,8 @@
},
thyheader => sub {
my ($file, @content) = @_;
- my $diag = 1;
- #~ my $diag = 0;
+ #~ my $diag = 1;
+ my $diag = 0;
$_ = join("", @content);
if (m!^theory!cgoms) {
my $prelude = $`;
--- a/doc-src/AxClass/Group/Group.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/AxClass/Group/Group.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* Basic group theory *}
-theory Group = Main:
+theory Group imports Main begin
text {*
\medskip\noindent The meta-level type system of Isabelle supports
--- a/doc-src/AxClass/Group/Product.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/AxClass/Group/Product.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* Syntactic classes *}
-theory Product = Main:
+theory Product imports Main begin
text {*
\medskip\noindent There is still a feature of Isabelle's type system
--- a/doc-src/AxClass/Group/Semigroups.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* Semigroups *}
-theory Semigroups = Main:
+theory Semigroups imports Main begin
text {*
\medskip\noindent An axiomatic type class is simply a class of types
--- a/doc-src/AxClass/Nat/NatClass.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/AxClass/Nat/NatClass.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* Defining natural numbers in FOL \label{sec:ex-natclass} *}
-theory NatClass = FOL:
+theory NatClass imports FOL begin
text {*
\medskip\noindent Axiomatic type classes abstract over exactly one
--- a/doc-src/IsarOverview/Isar/Calc.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/IsarOverview/Isar/Calc.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Calc = Main:
+theory Calc imports Main begin
subsection{* Chains of equalities *}
--- a/doc-src/Locales/Locales/Locales.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/Locales/Locales/Locales.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
*)
(*<*)
-theory Locales = Main:
+theory Locales imports Main begin
ML_setup {* print_mode := "type_brackets" :: !print_mode; *}
(*>*)
--- a/doc-src/TutorialI/Advanced/simp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory simp = Main:
+theory simp imports Main begin
(*>*)
section{*Simplification*}
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory CodeGen = Main:
+theory CodeGen imports Main begin
(*>*)
section{*Case Study: Compiling Expressions*}
--- a/doc-src/TutorialI/Datatype/ABexpr.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory ABexpr = Main:;
+theory ABexpr imports Main begin;
(*>*)
text{*
--- a/doc-src/TutorialI/Datatype/Fundata.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Fundata = Main:
+theory Fundata imports Main begin
(*>*)
datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Nested = ABexpr:
+theory Nested imports ABexpr begin
(*>*)
text{*
--- a/doc-src/TutorialI/Datatype/unfoldnested.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Datatype/unfoldnested.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory unfoldnested = Main:;
+theory unfoldnested imports Main begin;
(*>*)
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
--- a/doc-src/TutorialI/Documents/Documents.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Documents = Main:
+theory Documents imports Main begin
(*>*)
section {* Concrete Syntax \label{sec:concrete-syntax} *}
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Ifexpr = Main:;
+theory Ifexpr imports Main begin;
(*>*)
subsection{*Case Study: Boolean Expressions*}
--- a/doc-src/TutorialI/Inductive/Advanced.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Advanced = Even:
+theory Advanced imports Even begin
datatype 'f gterm = Apply 'f "'f gterm list"
--- a/doc-src/TutorialI/Inductive/Even.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Even = Main:
+theory Even imports Main begin
consts even :: "nat set"
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory AdvancedInd = Main:;
+theory AdvancedInd imports Main begin;
(*>*)
text{*\noindent
--- a/doc-src/TutorialI/Misc/Itrev.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Itrev = Main:;
+theory Itrev imports Main begin;
(*>*)
section{*Induction Heuristics*}
--- a/doc-src/TutorialI/Misc/Option2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Option2 = Main:
+theory Option2 imports Main begin
hide const None Some
hide type option
(*>*)
--- a/doc-src/TutorialI/Misc/Plus.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/Plus.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Plus = Main:
+theory Plus imports Main begin
(*>*)
text{*\noindent Define the following addition function *}
--- a/doc-src/TutorialI/Misc/Tree.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Tree = Main:
+theory Tree imports Main begin
(*>*)
text{*\noindent
--- a/doc-src/TutorialI/Misc/Tree2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/Tree2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Tree2 = Tree:
+theory Tree2 imports Tree begin
(*>*)
text{*\noindent In Exercise~\ref{ex:Tree} we defined a function
--- a/doc-src/TutorialI/Misc/appendix.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/appendix.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory appendix = Main:;
+theory appendix imports Main begin;
(*>*)
text{*
--- a/doc-src/TutorialI/Misc/case_exprs.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory case_exprs = Main:
+theory case_exprs imports Main begin
(*>*)
subsection{*Case Expressions*}
--- a/doc-src/TutorialI/Misc/fakenat.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/fakenat.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory fakenat = Main:;
+theory fakenat imports Main begin;
(*>*)
text{*\noindent
--- a/doc-src/TutorialI/Misc/natsum.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory natsum = Main:;
+theory natsum imports Main begin;
(*>*)
text{*\noindent
In particular, there are @{text"case"}-expressions, for example
--- a/doc-src/TutorialI/Misc/pairs.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory pairs = Main:;
+theory pairs imports Main begin;
(*>*)
text{*\label{sec:pairs}\index{pairs and tuples}
HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
--- a/doc-src/TutorialI/Misc/prime_def.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory prime_def = Main:;
+theory prime_def imports Main begin;
consts prime :: "nat \<Rightarrow> bool"
(*>*)
text{*
--- a/doc-src/TutorialI/Misc/simp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory simp = Main:
+theory simp imports Main begin
(*>*)
subsection{*Simplification Rules*}
--- a/doc-src/TutorialI/Overview/Isar.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Overview/Isar.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Isar = Sets:
+theory Isar imports Sets begin
section{*A Taste of Structured Proofs in Isar*}
--- a/doc-src/TutorialI/Overview/LNCS/FP0.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP0.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory FP0 = PreList:
+theory FP0 imports PreList begin
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
--- a/doc-src/TutorialI/Overview/LNCS/Ordinal.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Ordinal.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Ordinal = Main:
+theory Ordinal imports Main begin
datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
--- a/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory RECDEF = Main:
+theory RECDEF imports Main begin
(*>*)
subsection{*Wellfounded Recursion*}
--- a/doc-src/TutorialI/Protocol/Event.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,8 +11,8 @@
stores are visible to him
*)
-theory Event = Message
-files ("Event_lemmas.ML"):
+theory Event imports Message
+uses ("Event_lemmas.ML") begin
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
--- a/doc-src/TutorialI/Protocol/Message.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,8 +7,8 @@
Inductive relations "parts", "analz" and "synth"
*)
-theory Message = Main
-files ("Message_lemmas.ML"):
+theory Message imports Main
+uses ("Message_lemmas.ML") begin
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A Un (B Un A) = B Un A"
--- a/doc-src/TutorialI/Protocol/NS_Public.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Version incorporating Lowe's fix (inclusion of B's identity in round 2).
*)
-theory NS_Public = Public:
+theory NS_Public imports Public begin
consts ns_public :: "event list set"
--- a/doc-src/TutorialI/Protocol/Public.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,8 +8,8 @@
Private and public keys; initial states of agents
*)
-theory Public = Event
-files ("Public_lemmas.ML"):
+theory Public imports Event
+uses ("Public_lemmas.ML") begin
consts
pubK :: "agent => key"
--- a/doc-src/TutorialI/Recdef/Induction.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Induction = examples + simplification:;
+theory Induction imports examples simplification begin;
(*>*)
text{*
--- a/doc-src/TutorialI/Recdef/Nested0.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Nested0 = Main:
+theory Nested0 imports Main begin
(*>*)
text{*
--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Nested1 = Nested0:
+theory Nested1 imports Nested0 begin
(*>*)
text{*\noindent
--- a/doc-src/TutorialI/Recdef/Nested2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Nested2 = Nested0:
+theory Nested2 imports Nested0 begin
(*>*)
lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
--- a/doc-src/TutorialI/Recdef/examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory examples = Main:;
+theory examples imports Main begin;
(*>*)
text{*
--- a/doc-src/TutorialI/Recdef/simplification.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory simplification = Main:;
+theory simplification imports Main begin;
(*>*)
text{*
--- a/doc-src/TutorialI/Recdef/termination.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory termination = examples:
+theory termination imports examples begin
(*>*)
text{*
--- a/doc-src/TutorialI/Rules/Basic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Basic = Main:
+theory Basic imports Main begin
lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)"
apply (rule conjI)
--- a/doc-src/TutorialI/Rules/Blast.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Blast.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Blast = Main:
+theory Blast imports Main begin
lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y)))) =
((\<exists>x. \<forall>y. q(x)=q(y)) = ((\<exists>x. p(x))=(\<forall>y. q(y))))"
--- a/doc-src/TutorialI/Rules/Force.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Force = Main:
+theory Force imports Main begin
(*Use Divides rather than Main to experiment with the first proof.
Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
--- a/doc-src/TutorialI/Rules/Forward.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Forward = Primes:
+theory Forward imports Primes begin
text{*\noindent
Forward proof material: of, OF, THEN, simplify, rule_format.
--- a/doc-src/TutorialI/Rules/Primes.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
(*Euclid's algorithm
This material now appears AFTER that of Forward.thy *)
-theory Primes = Main:
+theory Primes imports Main begin
consts
gcd :: "nat*nat \<Rightarrow> nat"
--- a/doc-src/TutorialI/Rules/Tacticals.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Rules/Tacticals.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Tacticals = Main:
+theory Tacticals imports Main begin
text{*REPEAT*}
lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"
--- a/doc-src/TutorialI/Sets/Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Examples = Main:
+theory Examples imports Main begin
ML "reset eta_contract"
ML "Pretty.setmargin 64"
--- a/doc-src/TutorialI/Sets/Functions.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Functions = Main:
+theory Functions imports Main begin
ML "Pretty.setmargin 64"
--- a/doc-src/TutorialI/Sets/Recur.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Sets/Recur.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Recur = Main:
+theory Recur imports Main begin
ML "Pretty.setmargin 64"
--- a/doc-src/TutorialI/Sets/Relations.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Relations = Main:
+theory Relations imports Main begin
ML "Pretty.setmargin 64"
--- a/doc-src/TutorialI/Trie/Trie.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(*<*)
-theory Trie = Main:;
+theory Trie imports Main begin;
(*>*)
text{*
To minimize running time, each node of a trie should contain an array that maps
--- a/doc-src/TutorialI/Types/Numbers.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
(* ID: $Id$ *)
-theory Numbers = Real:
+theory Numbers imports Real begin
ML "Pretty.setmargin 64"
ML "IsarOutput.indent := 0" (*we don't want 5 for listing theorems*)
--- a/doc-src/TutorialI/Types/Records.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/TutorialI/Types/Records.thy Fri Jun 17 16:12:49 2005 +0200
@@ -2,7 +2,7 @@
header {* Records \label{sec:records} *}
(*<*)
-theory Records = Main:
+theory Records imports Main begin
(*>*)
text {*
--- a/doc-src/ZF/FOL_examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/ZF/FOL_examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header{*Examples of Classical Reasoning*}
-theory FOL_examples = FOL:
+theory FOL_examples imports FOL begin
lemma "EX y. ALL x. P(y)-->P(x)"
--{* @{subgoals[display,indent=0,margin=65]} *}
--- a/doc-src/ZF/IFOL_examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/ZF/IFOL_examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header{*Examples of Intuitionistic Reasoning*}
-theory IFOL_examples = IFOL:
+theory IFOL_examples imports IFOL begin
text{*Quantifier example from the book Logic and Computation*}
lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
--- a/doc-src/ZF/If.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/ZF/If.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
First-Order Logic: the 'if' example.
*)
-theory If = FOL:
+theory If imports FOL begin
constdefs
if :: "[o,o,o]=>o"
--- a/doc-src/ZF/ZF_examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/doc-src/ZF/ZF_examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header{*Examples of Reasoning in ZF Set Theory*}
-theory ZF_examples = Main_ZFC:
+theory ZF_examples imports Main_ZFC begin
subsection {* Binary Trees *}
--- a/src/CTT/Main.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/CTT/Main.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(*theory Main includes everything*)
-theory Main = CTT + Arith + Bool:
+theory Main imports CTT Arith Bool begin
end
--- a/src/FOL/FOL.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/FOL.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory FOL
imports IFOL
-files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
("eqrule_FOL_data.ML")
("~~/src/Provers/eqsubst.ML")
begin
--- a/src/FOL/IFOL.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/IFOL.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory IFOL
imports Pure
-files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
+uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
begin
--- a/src/FOL/ex/Classical.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/Classical.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Classical Predicate Calculus Problems*}
-theory Classical = FOL:
+theory Classical imports FOL begin
lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
by blast
--- a/src/FOL/ex/First_Order_Logic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/First_Order_Logic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* A simple formulation of First-Order Logic *}
-theory First_Order_Logic = Pure:
+theory First_Order_Logic imports Pure begin
text {*
The subsequent theory development illustrates single-sorted
--- a/src/FOL/ex/If.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/If.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* First-Order Logic: the 'if' example *}
-theory If = FOL:
+theory If imports FOL begin
constdefs
if :: "[o,o,o]=>o"
--- a/src/FOL/ex/IffOracle.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/IffOracle.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Example of Declaring an Oracle*}
-theory IffOracle = FOL:
+theory IffOracle imports FOL begin
text{*This oracle makes tautologies of the form "P <-> P <-> P <-> P".
The length is specified by an integer, which is checked to be even and
--- a/src/FOL/ex/Intuitionistic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/Intuitionistic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Intuitionistic First-Order Logic*}
-theory Intuitionistic = IFOL:
+theory Intuitionistic imports IFOL begin
(*
Single-step ML commands:
--- a/src/FOL/ex/Natural_Numbers.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/Natural_Numbers.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Natural numbers *}
-theory Natural_Numbers = FOL:
+theory Natural_Numbers imports FOL begin
text {*
Theory of the natural numbers: Peano's axioms, primitive recursion.
--- a/src/FOL/ex/int.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/FOL/ex/int.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,6 +6,6 @@
Intuitionistic First-Order Logic.
*)
-theory int = IFOL:
+theory int imports IFOL begin
end
--- a/src/HOL/Algebra/Bij.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Bij.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
-theory Bij = Group:
+theory Bij imports Group begin
constdefs
Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
--- a/src/HOL/Algebra/CRing.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/CRing.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,8 +7,8 @@
header {* Abelian Groups *}
-theory CRing = FiniteProduct
-files ("ringsimp.ML"):
+theory CRing imports FiniteProduct
+uses ("ringsimp.ML") begin
record 'a ring = "'a monoid" +
zero :: 'a ("\<zero>\<index>")
--- a/src/HOL/Algebra/Coset.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*Cosets and Quotient Groups*}
-theory Coset = Group + Exponent:
+theory Coset imports Group Exponent begin
constdefs (structure G)
r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "#>\<index>" 60)
--- a/src/HOL/Algebra/Exponent.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Exponent.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
-theory Exponent = Main + Primes:
+theory Exponent imports Main Primes begin
constdefs
exponent :: "[nat, nat] => nat"
--- a/src/HOL/Algebra/FiniteProduct.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Product Operator for Commutative Monoids *}
-theory FiniteProduct = Group:
+theory FiniteProduct imports Group begin
text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
possible, because here we have explicit typing rules like
--- a/src/HOL/Algebra/Group.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Group.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* Groups *}
-theory Group = FuncSet + Lattice:
+theory Group imports FuncSet Lattice begin
section {* Monoids and Groups *}
--- a/src/HOL/Algebra/Lattice.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Lattice.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Orders and Lattices *}
-theory Lattice = Main:
+theory Lattice imports Main begin
text {* Object with a carrier set. *}
--- a/src/HOL/Algebra/Module.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Module.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Modules over an Abelian Group *}
-theory Module = CRing:
+theory Module imports CRing begin
record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
--- a/src/HOL/Algebra/Sylow.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Sylow.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Sylow's theorem *}
-theory Sylow = Coset:
+theory Sylow imports Coset begin
text {*
See also \cite{Kammueller-Paulson:1999}.
--- a/src/HOL/Algebra/UnivPoly.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Univariate Polynomials *}
-theory UnivPoly = Module:
+theory UnivPoly imports Module begin
text {*
Polynomials are formalised as modules with additional operations for
--- a/src/HOL/Algebra/abstract/Abstract.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Abstract.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,6 +4,6 @@
Author: Clemens Ballarin, started 17 July 1997
*)
-theory Abstract = RingHomo + Field:
+theory Abstract imports RingHomo Field begin
end
--- a/src/HOL/Algebra/abstract/Ring.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,8 +7,8 @@
header {* The algebraic hierarchy of rings as axiomatic classes *}
-theory Ring = Main
-files ("order.ML"):
+theory Ring imports Main
+uses ("order.ML") begin
section {* Constants *}
--- a/src/HOL/Algebra/poly/LongDiv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Author: Clemens Ballarin, started 23 June 1999
*)
-theory LongDiv = PolyHomo:
+theory LongDiv imports PolyHomo begin
consts
lcoeff :: "'a::ring up => 'a"
--- a/src/HOL/Auth/CertifiedEmail.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*The Certified Electronic Mail Protocol by Abadi et al.*}
-theory CertifiedEmail = Public:
+theory CertifiedEmail imports Public begin
syntax
TTP :: agent
--- a/src/HOL/Auth/Event.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Event.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Theory of Events for Security Protocols*}
-theory Event = Message:
+theory Event imports Message begin
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
--- a/src/HOL/Auth/Guard/Analz.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Analz.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Decomposition of Analz into two parts*}
-theory Analz = Extensions:
+theory Analz imports Extensions begin
text{*decomposition of @{term analz} into two parts:
@{term pparts} (for pairs) and analz of @{term kparts}*}
--- a/src/HOL/Auth/Guard/Extensions.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header {*Extensions to Standard Theories*}
-theory Extensions = Event:
+theory Extensions imports Event begin
subsection{*Extensions to Theory @{text Set}*}
--- a/src/HOL/Auth/Guard/Guard.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Protocol-Independent Confidentiality Theorem on Nonces*}
-theory Guard = Analz + Extensions:
+theory Guard imports Analz Extensions begin
(******************************************************************************
messages where all the occurrences of Nonce n are
--- a/src/HOL/Auth/Guard/GuardK.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
header{*protocol-independent confidentiality theorem on keys*}
-theory GuardK = Analz + Extensions:
+theory GuardK imports Analz Extensions begin
(******************************************************************************
messages where all the occurrences of Key n are
--- a/src/HOL/Auth/Guard/Guard_Public.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
Cambridge CB3 0FD, United Kingdom
******************************************************************************)
-theory Guard_Public = Guard + Public + Extensions:
+theory Guard_Public imports Guard Public Extensions begin
subsection{*Extensions to Theory @{text Public}*}
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*lemmas on guarded messages for protocols with symmetric keys*}
-theory Guard_Shared = Guard + GuardK + Shared:
+theory Guard_Shared imports Guard GuardK Shared begin
subsection{*Extensions to Theory @{text Shared}*}
--- a/src/HOL/Auth/Guard/List_Msg.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/List_Msg.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Lists of Messages and Lists of Agents*}
-theory List_Msg = Extensions:
+theory List_Msg imports Extensions begin
subsection{*Implementation of Lists by Messages*}
--- a/src/HOL/Auth/Guard/NS_Public.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/NS_Public.thy Fri Jun 17 16:12:49 2005 +0200
@@ -13,7 +13,7 @@
header{*Needham-Schroeder-Lowe Public-Key Protocol*}
-theory NS_Public = Guard_Public:
+theory NS_Public imports Guard_Public begin
subsection{*messages used in the protocol*}
--- a/src/HOL/Auth/Guard/OtwayRees.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/OtwayRees.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Otway-Rees Protocol*}
-theory OtwayRees = Guard_Shared:
+theory OtwayRees imports Guard_Shared begin
subsection{*messages used in the protocol*}
--- a/src/HOL/Auth/Guard/P1.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/P1.thy Fri Jun 17 16:12:49 2005 +0200
@@ -15,7 +15,7 @@
header{*Protocol P1*}
-theory P1 = Guard_Public + List_Msg:
+theory P1 imports Guard_Public List_Msg begin
subsection{*Protocol Definition*}
--- a/src/HOL/Auth/Guard/P2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/P2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -15,7 +15,7 @@
header{*Protocol P2*}
-theory P2 = Guard_Public + List_Msg:
+theory P2 imports Guard_Public List_Msg begin
subsection{*Protocol Definition*}
--- a/src/HOL/Auth/Guard/Proto.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Other Protocol-Independent Results*}
-theory Proto = Guard_Public:
+theory Proto imports Guard_Public begin
subsection{*protocols*}
--- a/src/HOL/Auth/Guard/Yahalom.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Guard/Yahalom.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Yahalom Protocol*}
-theory Yahalom = Guard_Shared:
+theory Yahalom imports Guard_Shared begin
subsection{*messages used in the protocol*}
--- a/src/HOL/Auth/KerberosIV.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Kerberos Protocol, Version IV*}
-theory KerberosIV = Public:
+theory KerberosIV imports Public begin
syntax
Kas :: agent
--- a/src/HOL/Auth/Kerberos_BAN.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*The Kerberos Protocol, BAN Version*}
-theory Kerberos_BAN = Public:
+theory Kerberos_BAN imports Public begin
text{*From page 251 of
Burrows, Abadi and Needham (1989). A Logic of Authentication.
--- a/src/HOL/Auth/Message.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Message.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header{*Theory of Agents and Messages for Security Protocols*}
-theory Message = Main:
+theory Message imports Main begin
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
--- a/src/HOL/Auth/NS_Public.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/NS_Public.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header{*Verifying the Needham-Schroeder-Lowe Public-Key Protocol*}
-theory NS_Public = Public:
+theory NS_Public imports Public begin
consts ns_public :: "event list set"
--- a/src/HOL/Auth/NS_Public_Bad.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Jun 17 16:12:49 2005 +0200
@@ -13,7 +13,7 @@
header{*Verifying the Needham-Schroeder Public-Key Protocol*}
-theory NS_Public_Bad = Public:
+theory NS_Public_Bad imports Public begin
consts ns_public :: "event list set"
--- a/src/HOL/Auth/NS_Shared.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Needham-Schroeder Shared-Key Protocol*}
-theory NS_Shared = Public:
+theory NS_Shared imports Public begin
text{*
From page 247 of
--- a/src/HOL/Auth/OtwayRees.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Original Otway-Rees Protocol*}
-theory OtwayRees = Public:
+theory OtwayRees imports Public begin
text{* From page 244 of
Burrows, Abadi and Needham (1989). A Logic of Authentication.
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Otway-Rees Protocol as Modified by Abadi and Needham*}
-theory OtwayRees_AN = Public:
+theory OtwayRees_AN imports Public begin
text{*
This simplified version has minimal encryption and explicit messages.
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*The Otway-Rees Protocol: The Faulty BAN Version*}
-theory OtwayRees_Bad = Public:
+theory OtwayRees_Bad imports Public begin
text{*The FAULTY version omitting encryption of Nonce NB, as suggested on
page 247 of
--- a/src/HOL/Auth/Public.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Public.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
Private and public keys; initial states of agents
*)
-theory Public = Event:
+theory Public imports Event begin
lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
by (simp add: symKeys_def)
--- a/src/HOL/Auth/Recur.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Otway-Bull Recursive Authentication Protocol*}
-theory Recur = Public:
+theory Recur imports Public begin
text{*End marker for message bundles*}
syntax END :: "msg"
--- a/src/HOL/Auth/Shared.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Shared.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
Shared, long-term keys; initial states of agents
*)
-theory Shared = Event:
+theory Shared imports Event begin
consts
shrK :: "agent => key" (*symmetric keys*);
--- a/src/HOL/Auth/TLS.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/TLS.thy Fri Jun 17 16:12:49 2005 +0200
@@ -41,7 +41,7 @@
header{*The TLS Protocol: Transport Layer Security*}
-theory TLS = Public + NatPair:
+theory TLS imports Public NatPair begin
constdefs
certificate :: "[agent,key] => msg"
--- a/src/HOL/Auth/WooLam.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/WooLam.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Woo-Lam Protocol*}
-theory WooLam = Public:
+theory WooLam imports Public begin
text{*Simplified version from page 11 of
Abadi and Needham (1996).
--- a/src/HOL/Auth/Yahalom.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Yahalom Protocol*}
-theory Yahalom = Public:
+theory Yahalom imports Public begin
text{*From page 257 of
Burrows, Abadi and Needham (1989). A Logic of Authentication.
--- a/src/HOL/Auth/Yahalom2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Yahalom Protocol, Variant 2*}
-theory Yahalom2 = Public:
+theory Yahalom2 imports Public begin
text{*
This version trades encryption of NB for additional explicitness in YM3.
--- a/src/HOL/Auth/Yahalom_Bad.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Yahalom Protocol: A Flawed Version*}
-theory Yahalom_Bad = Public:
+theory Yahalom_Bad imports Public begin
text{*
Demonstrates of why Oops is necessary. This protocol can be attacked because
--- a/src/HOL/Auth/ZhouGollmann.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
55-61
*)
-theory ZhouGollmann = Public:
+theory ZhouGollmann imports Public begin
syntax
TTP :: agent
--- a/src/HOL/AxClasses/Group.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/AxClasses/Group.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-theory Group = Main:
+theory Group imports Main begin
subsection {* Monoids and Groups *}
--- a/src/HOL/AxClasses/Product.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/AxClasses/Product.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-theory Product = Main:
+theory Product imports Main begin
axclass product < type
--- a/src/HOL/AxClasses/Semigroups.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/AxClasses/Semigroups.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-theory Semigroups = Main:
+theory Semigroups imports Main begin
consts
times :: "'a => 'a => 'a" (infixl "[*]" 70)
--- a/src/HOL/Bali/AxCompl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/AxCompl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Completeness proof for Axiomatic semantics of Java expressions and statements
*}
-theory AxCompl = AxSem:
+theory AxCompl imports AxSem begin
text {*
design issues:
--- a/src/HOL/Bali/AxExample.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/AxExample.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Example of a proof based on the Bali axiomatic semantics *}
-theory AxExample = AxSem + Example:
+theory AxExample imports AxSem Example begin
constdefs
arr_inv :: "st \<Rightarrow> bool"
--- a/src/HOL/Bali/AxSem.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/AxSem.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
(see also Eval.thy)
*}
-theory AxSem = Evaln + TypeSafe:
+theory AxSem imports Evaln TypeSafe begin
text {*
design issues:
--- a/src/HOL/Bali/AxSound.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/AxSound.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
-theory AxSound = AxSem:
+theory AxSound imports AxSem begin
section "validity"
--- a/src/HOL/Bali/Basis.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Basis.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
*)
header {* Definitions extending HOL as logical basis of Bali *}
-theory Basis = Main:
+theory Basis imports Main begin
ML {*
Unify.search_bound := 40;
--- a/src/HOL/Bali/Conform.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Conform.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Conformance notions for the type soundness proof for Java *}
-theory Conform = State:
+theory Conform imports State begin
text {*
design issues:
--- a/src/HOL/Bali/Decl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Decl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
*}
(** order is significant, because of clash for "var" **)
-theory Decl = Term + Table:
+theory Decl imports Term Table begin
text {*
improvements:
--- a/src/HOL/Bali/DeclConcepts.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Advanced concepts on Java declarations like overriding, inheritance,
dynamic method lookup*}
-theory DeclConcepts = TypeRel:
+theory DeclConcepts imports TypeRel begin
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
--- a/src/HOL/Bali/DefiniteAssignment.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header {* Definite Assignment *}
-theory DefiniteAssignment = WellType:
+theory DefiniteAssignment imports WellType begin
text {* Definite Assignment Analysis (cf. 16)
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header {* Correctness of Definite Assignment *}
-theory DefiniteAssignmentCorrect = WellForm + Eval:
+theory DefiniteAssignmentCorrect imports WellForm Eval begin
ML {*
Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
--- a/src/HOL/Bali/Eval.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Eval.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
statements
*}
-theory Eval = State + DeclConcepts:
+theory Eval imports State DeclConcepts begin
text {*
--- a/src/HOL/Bali/Evaln.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Evaln.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
statements
*}
-theory Evaln = TypeSafe:
+theory Evaln imports TypeSafe begin
text {*
--- a/src/HOL/Bali/Example.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Example.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* Example Bali program *}
-theory Example = Eval + WellForm:
+theory Example imports Eval WellForm begin
text {*
The following example Bali program includes:
--- a/src/HOL/Bali/Name.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Name.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* Java names *}
-theory Name = Basis:
+theory Name imports Basis begin
(* cf. 6.5 *)
typedecl tnam --{* ordinary type name, i.e. class or interface name *}
--- a/src/HOL/Bali/State.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/State.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* State for evaluation of Java expressions and statements *}
-theory State = DeclConcepts:
+theory State imports DeclConcepts begin
text {*
design issues:
--- a/src/HOL/Bali/Table.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Table.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* Abstract tables and their implementation as lists *}
-theory Table = Basis:
+theory Table imports Basis begin
text {*
design issues:
--- a/src/HOL/Bali/Term.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Term.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Java expressions and statements *}
-theory Term = Value + Table:
+theory Term imports Value Table begin
text {*
design issues:
--- a/src/HOL/Bali/Trans.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Trans.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
PRELIMINARY!!!!!!!!
*)
-theory Trans = Evaln:
+theory Trans imports Evaln begin
constdefs groundVar:: "var \<Rightarrow> bool"
"groundVar v \<equiv> (case v of
--- a/src/HOL/Bali/Type.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Type.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Java types *}
-theory Type = Name:
+theory Type imports Name begin
text {*
simplifications:
--- a/src/HOL/Bali/TypeRel.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/TypeRel.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* The relations between Java types *}
-theory TypeRel = Decl:
+theory TypeRel imports Decl begin
text {*
simplifications:
--- a/src/HOL/Bali/TypeSafe.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* The type soundness proof for Java *}
-theory TypeSafe = DefiniteAssignmentCorrect + Conform:
+theory TypeSafe imports DefiniteAssignmentCorrect Conform begin
section "error free"
--- a/src/HOL/Bali/Value.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/Value.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
-theory Value = Type:
+theory Value imports Type begin
typedecl loc --{* locations, i.e. abstract references on objects *}
arities loc :: "type"
--- a/src/HOL/Bali/WellForm.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/WellForm.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* Well-formedness of Java programs *}
-theory WellForm = DefiniteAssignment:
+theory WellForm imports DefiniteAssignment begin
text {*
For static checks on expressions and statements, see WellType.thy
--- a/src/HOL/Bali/WellType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Bali/WellType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
header {* Well-typedness of Java programs *}
-theory WellType = DeclConcepts:
+theory WellType imports DeclConcepts begin
text {*
improvements over Java Specification 1.0:
--- a/src/HOL/Extraction.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Extraction.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Extraction
imports Datatype
-files "Tools/rewrite_hol_proof.ML"
+uses "Tools/rewrite_hol_proof.ML"
begin
subsection {* Setup *}
--- a/src/HOL/Extraction/Higman.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Extraction/Higman.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Higman's lemma *}
-theory Higman = Main:
+theory Higman imports Main begin
text {*
Formalization by Stefan Berghofer and Monika Seisenberger,
--- a/src/HOL/Extraction/QuotRem.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Extraction/QuotRem.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Quotient and remainder *}
-theory QuotRem = Main:
+theory QuotRem imports Main begin
text {* Derivation of quotient and remainder using program extraction. *}
--- a/src/HOL/Extraction/Warshall.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Extraction/Warshall.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Warshall's algorithm *}
-theory Warshall = Main:
+theory Warshall imports Main begin
text {*
Derivation of Warshall's algorithm using program extraction,
--- a/src/HOL/HOL.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HOL.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory HOL
imports CPure
-files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
+uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
("~~/src/Provers/eqsubst.ML")
begin
--- a/src/HOL/Hilbert_Choice.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
theory Hilbert_Choice
imports NatArith
-files ("Tools/meson.ML") ("Tools/specification_package.ML")
+uses ("Tools/meson.ML") ("Tools/specification_package.ML")
begin
subsection {* Hilbert's epsilon *}
--- a/src/HOL/Hoare/Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
Various examples.
*)
-theory Examples = Hoare + Arith2:
+theory Examples imports Hoare Arith2 begin
(*** ARITHMETIC ***)
--- a/src/HOL/Hoare/ExamplesAbort.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/ExamplesAbort.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
Some small examples for programs that may abort.
*)
-theory ExamplesAbort = HoareAbort:
+theory ExamplesAbort imports HoareAbort begin
lemma "VARS x y z::nat
{y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
--- a/src/HOL/Hoare/Heap.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Heap.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
See the paper by Mehta and Nipkow.
*)
-theory Heap = Main:
+theory Heap imports Main begin
subsection "References"
--- a/src/HOL/Hoare/HeapSyntax.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/HeapSyntax.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 2002 TUM
*)
-theory HeapSyntax = Hoare + Heap:
+theory HeapSyntax imports Hoare Heap begin
subsection "Field access and update"
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 2002 TUM
*)
-theory HeapSyntaxAbort = HoareAbort + Heap:
+theory HeapSyntaxAbort imports HoareAbort Heap begin
subsection "Field access and update"
--- a/src/HOL/Hoare/Hoare.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Hoare.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,8 +9,8 @@
later.
*)
-theory Hoare = Main
-files ("hoare.ML"):
+theory Hoare imports Main
+uses ("hoare.ML") begin
types
'a bexp = "'a set"
--- a/src/HOL/Hoare/HoareAbort.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,8 +6,8 @@
Like Hoare.thy, but with an Abort statement for modelling run time errors.
*)
-theory HoareAbort = Main
-files ("hoareAbort.ML"):
+theory HoareAbort imports Main
+uses ("hoareAbort.ML") begin
types
'a bexp = "'a set"
--- a/src/HOL/Hoare/Pointer_Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
Examples of verifications of pointer programs
*)
-theory Pointer_Examples = HeapSyntax:
+theory Pointer_Examples imports HeapSyntax begin
section "Verifications"
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
Examples of verifications of pointer programs
*)
-theory Pointer_ExamplesAbort = HeapSyntaxAbort:
+theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
section "Verifications"
--- a/src/HOL/Hoare/Pointers0.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Pointers0.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
- in fact in some case they appear to get (a bit) more complicated.
*)
-theory Pointers0 = Hoare:
+theory Pointers0 imports Hoare begin
subsection "References"
--- a/src/HOL/Hoare/SchorrWaite.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
*)
-theory SchorrWaite = HeapSyntax:
+theory SchorrWaite imports HeapSyntax begin
section {* Machinery for the Schorr-Waite proof*}
--- a/src/HOL/Hoare/SepLogHeap.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/SepLogHeap.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
for Separation Logic.
*)
-theory SepLogHeap = Main:
+theory SepLogHeap imports Main begin
types heap = "(nat \<Rightarrow> nat option)"
--- a/src/HOL/Hoare/Separation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hoare/Separation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -13,7 +13,7 @@
*)
-theory Separation = HoareAbort + SepLogHeap:
+theory Separation imports HoareAbort SepLogHeap begin
text{* The semantic definition of a few connectives: *}
--- a/src/HOL/HoareParallel/Gar_Coll.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* \section{The Single Mutator Case} *}
-theory Gar_Coll = Graph + OG_Syntax:
+theory Gar_Coll imports Graph OG_Syntax begin
declare psubsetE [rule del]
--- a/src/HOL/HoareParallel/Graph.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
\section {Formalization of the Memory} *}
-theory Graph = Main:
+theory Graph imports Main begin
datatype node = Black | White
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* \section{The Multi-Mutator Case} *}
-theory Mul_Gar_Coll = Graph + OG_Syntax:
+theory Mul_Gar_Coll imports Graph OG_Syntax begin
text {* The full theory takes aprox. 18 minutes. *}
--- a/src/HOL/HoareParallel/OG_Com.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/OG_Com.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
\section{Abstract Syntax} *}
-theory OG_Com = Main:
+theory OG_Com imports Main begin
text {* Type abbreviations for boolean expressions and assertions: *}
--- a/src/HOL/HoareParallel/OG_Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* \section{Examples} *}
-theory OG_Examples = OG_Syntax:
+theory OG_Examples imports OG_Syntax begin
subsection {* Mutual Exclusion *}
--- a/src/HOL/HoareParallel/OG_Hoare.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/OG_Hoare.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* \section{The Proof System} *}
-theory OG_Hoare = OG_Tran:
+theory OG_Hoare imports OG_Tran begin
consts assertions :: "'a ann_com \<Rightarrow> ('a assn) set"
primrec
--- a/src/HOL/HoareParallel/OG_Tran.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/OG_Tran.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* \section{Operational Semantics} *}
-theory OG_Tran = OG_Com:
+theory OG_Tran imports OG_Com begin
types
'a ann_com_op = "('a ann_com) option"
--- a/src/HOL/HoareParallel/Quote_Antiquote.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/Quote_Antiquote.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* \section{Concrete Syntax} *}
-theory Quote_Antiquote = Main:
+theory Quote_Antiquote imports Main begin
syntax
"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
--- a/src/HOL/HoareParallel/RG_Com.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Com.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
\section {Abstract Syntax}
*}
-theory RG_Com = Main:
+theory RG_Com imports Main begin
text {* Semantics of assertions and boolean expressions (bexp) as sets
of states. Syntax of commands @{text com} and parallel commands
--- a/src/HOL/HoareParallel/RG_Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header {* \section{Examples} *}
-theory RG_Examples = RG_Syntax:
+theory RG_Examples imports RG_Syntax begin
lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def
--- a/src/HOL/HoareParallel/RG_Hoare.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
header {* \section{The Proof System} *}
-theory RG_Hoare = RG_Tran:
+theory RG_Hoare imports RG_Tran begin
subsection {* Proof System for Component Programs *}
--- a/src/HOL/Hyperreal/HyperArith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
theory HyperArith
imports HyperDef
-files ("hypreal_arith.ML")
+uses ("hypreal_arith.ML")
begin
subsection{*Numerals and Arithmetic*}
--- a/src/HOL/Hyperreal/HyperDef.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
theory HyperDef
imports Filter "../Real/Real"
-files ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*)
+uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*)
begin
constdefs
--- a/src/HOL/IMP/Com.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Com.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header "Syntax of Commands"
-theory Com = Main:
+theory Com imports Main begin
typedecl loc
-- "an unspecified (arbitrary) type of locations
--- a/src/HOL/IMP/Compiler.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Compiler.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1996 TUM
*)
-theory Compiler = Machines:
+theory Compiler imports Machines begin
subsection "The compiler"
--- a/src/HOL/IMP/Compiler0.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Compiler0.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header "A Simple Compiler"
-theory Compiler0 = Natural:
+theory Compiler0 imports Natural begin
subsection "An abstract, simplistic machine"
--- a/src/HOL/IMP/Denotation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Denotation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Denotational Semantics of Commands"
-theory Denotation = Natural:
+theory Denotation imports Natural begin
types com_den = "(state\<times>state)set"
--- a/src/HOL/IMP/Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Examples"
-theory Examples = Natural:
+theory Examples imports Natural begin
constdefs
factorial :: "loc => loc => com"
--- a/src/HOL/IMP/Expr.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Expr.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Expressions"
-theory Expr = Main:
+theory Expr imports Main begin
text {*
Arithmetic expressions and Boolean expressions.
--- a/src/HOL/IMP/Hoare.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Hoare.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Inductive Definition of Hoare Logic"
-theory Hoare = Denotation:
+theory Hoare imports Denotation begin
types assn = "state => bool"
--- a/src/HOL/IMP/Machines.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Machines.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory Machines = Natural:
+theory Machines imports Natural begin
lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
by(fast intro:rtrancl.intros elim:rtranclE)
--- a/src/HOL/IMP/Natural.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Natural.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header "Natural Semantics of Commands"
-theory Natural = Com:
+theory Natural imports Com begin
subsection "Execution of commands"
--- a/src/HOL/IMP/Transition.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/Transition.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header "Transition Semantics of Commands"
-theory Transition = Natural:
+theory Transition imports Natural begin
subsection "The transition relation"
--- a/src/HOL/IMP/VC.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/IMP/VC.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header "Verification Conditions"
-theory VC = Hoare:
+theory VC imports Hoare begin
datatype acom = Askip
| Aass loc aexp
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory GenHOL4Base = "../HOL4Compat" + "../HOL4Syntax":;
+theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;
import_segment "hol4";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory GenHOL4Prob = GenHOL4Real:
+theory GenHOL4Prob imports GenHOL4Real begin
import_segment "hol4";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory GenHOL4Real = GenHOL4Base:
+theory GenHOL4Real imports GenHOL4Base begin
import_segment "hol4";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory GenHOL4Vec = GenHOL4Base:
+theory GenHOL4Vec imports GenHOL4Base begin
import_segment "hol4";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory GenHOL4Word32 = GenHOL4Base:;
+theory GenHOL4Word32 imports GenHOL4Base begin;
import_segment "hol4";
--- a/src/HOL/Import/HOL/HOL4.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,6 +3,6 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4 = HOL4Vec + HOL4Word32 + HOL4Real:
+theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin
end
--- a/src/HOL/Import/HOL/HOL4Base.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":
+theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
;setup_theory bool
--- a/src/HOL/Import/HOL/HOL4Prob.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Prob = HOL4Real:
+theory HOL4Prob imports HOL4Real begin
;setup_theory prob_extra
--- a/src/HOL/Import/HOL/HOL4Real.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Real = HOL4Base:
+theory HOL4Real imports HOL4Base begin
;setup_theory realax
--- a/src/HOL/Import/HOL/HOL4Vec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Vec = HOL4Base:
+theory HOL4Vec imports HOL4Base begin
;setup_theory res_quan
--- a/src/HOL/Import/HOL/HOL4Word32.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-theory HOL4Word32 = HOL4Base:
+theory HOL4Word32 imports HOL4Base begin
;setup_theory bits
--- a/src/HOL/Import/HOL4Compat.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Compat = HOL4Setup + Divides + Primes + Real:
+theory HOL4Compat imports HOL4Setup Divides Primes Real begin
lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
by auto
--- a/src/HOL/Import/HOL4Setup.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL4Setup.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,8 +3,8 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Setup = MakeEqual
- files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
+theory HOL4Setup imports MakeEqual
+ uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
section {* General Setup *}
--- a/src/HOL/Import/HOL4Syntax.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/HOL4Syntax.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,8 +3,8 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Syntax = HOL4Setup
- files "import_syntax.ML":
+theory HOL4Syntax imports HOL4Setup
+ uses "import_syntax.ML" begin
ML {* HOL4ImportSyntax.setup() *}
--- a/src/HOL/Import/MakeEqual.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Import/MakeEqual.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,8 +3,8 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory MakeEqual = Main
- files "shuffler.ML":
+theory MakeEqual imports Main
+ uses "shuffler.ML" begin
setup Shuffler.setup
--- a/src/HOL/Induct/ABexp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/ABexp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Arithmetic and boolean expressions *}
-theory ABexp = Main:
+theory ABexp imports Main begin
datatype 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
--- a/src/HOL/Induct/Com.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Com.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Mutual Induction via Iteratived Inductive Definitions*}
-theory Com = Main:
+theory Com imports Main begin
typedecl loc
--- a/src/HOL/Induct/Comb.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Comb.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Combinatory Logic example: the Church-Rosser Theorem *}
-theory Comb = Main:
+theory Comb imports Main begin
text {*
Curiously, combinators do not include free variables.
--- a/src/HOL/Induct/LFilter.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/LFilter.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {*The "filter" functional for coinductive lists
--defined by a combination of induction and coinduction*}
-theory LFilter = LList:
+theory LFilter imports LList begin
consts
findRel :: "('a => bool) => ('a llist * 'a llist)set"
--- a/src/HOL/Induct/LList.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/LList.thy Fri Jun 17 16:12:49 2005 +0200
@@ -22,7 +22,7 @@
header {*Definition of type llist by a greatest fixed point*}
-theory LList = Main + SList:
+theory LList imports Main SList begin
consts
--- a/src/HOL/Induct/Mutil.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Mutil.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* The Mutilated Chess Board Problem *}
-theory Mutil = Main:
+theory Mutil imports Main begin
text {*
The Mutilated Chess Board Problem, formalized inductively.
--- a/src/HOL/Induct/Ordinals.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Ordinals.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Ordinals *}
-theory Ordinals = Main:
+theory Ordinals imports Main begin
text {*
Some basic definitions of ordinal numbers. Draws an Agda
--- a/src/HOL/Induct/PropLog.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/PropLog.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Meta-theory of propositional logic *}
-theory PropLog = Main:
+theory PropLog imports Main begin
text {*
Datatype definition of propositional logic formulae and inductive
--- a/src/HOL/Induct/QuoDataType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Defining an Initial Algebra by Quotienting a Free Algebra*}
-theory QuoDataType = Main:
+theory QuoDataType imports Main begin
subsection{*Defining the Free Algebra*}
--- a/src/HOL/Induct/QuoNestedDataType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Quotienting a Free Algebra Involving Nested Recursion*}
-theory QuoNestedDataType = Main:
+theory QuoNestedDataType imports Main begin
subsection{*Defining the Free Algebra*}
--- a/src/HOL/Induct/SList.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/SList.thy Fri Jun 17 16:12:49 2005 +0200
@@ -24,7 +24,7 @@
Tidied by lcp. Still needs removal of nat_rec.
*)
-theory SList = NatArith + Sexp + Hilbert_Choice:
+theory SList imports NatArith Sexp Hilbert_Choice begin
(*Hilbert_Choice is needed for the function "inv"*)
--- a/src/HOL/Induct/Sexp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Sexp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
structures by hand.
*)
-theory Sexp = Datatype_Universe + Inductive:
+theory Sexp imports Datatype_Universe Inductive begin
consts
sexp :: "'a item set"
--- a/src/HOL/Induct/Sigma_Algebra.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Sigma_Algebra.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Sigma algebras *}
-theory Sigma_Algebra = Main:
+theory Sigma_Algebra imports Main begin
text {*
This is just a tiny example demonstrating the use of inductive
--- a/src/HOL/Induct/Term.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Term.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Terms over a given alphabet *}
-theory Term = Main:
+theory Term imports Main begin
datatype ('a, 'b) "term" =
Var 'a
--- a/src/HOL/Induct/Tree.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Tree.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Infinitely branching trees *}
-theory Tree = Main:
+theory Tree imports Main begin
datatype 'a tree =
Atom 'a
--- a/src/HOL/Inductive.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Inductive.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Inductive
imports Gfp Sum_Type Relation Record
-files
+uses
("Tools/inductive_package.ML")
("Tools/inductive_realizer.ML")
("Tools/inductive_codegen.ML")
--- a/src/HOL/Integ/IntArith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Integ/IntArith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory IntArith
imports Numeral
-files ("int_arith1.ML")
+uses ("int_arith1.ML")
begin
text{*Duplicate: can't understand why it's necessary*}
--- a/src/HOL/Integ/IntDiv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Integ/IntDiv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
theory IntDiv
imports IntArith Recdef
-files ("IntDiv_setup.ML")
+uses ("IntDiv_setup.ML")
begin
declare zless_nat_conj [simp]
--- a/src/HOL/Integ/NatSimprocs.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory NatSimprocs
imports NatBin
-files "int_factor_simprocs.ML" "nat_simprocs.ML"
+uses "int_factor_simprocs.ML" "nat_simprocs.ML"
begin
setup nat_simprocs_setup
--- a/src/HOL/Integ/Numeral.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Integ/Numeral.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
theory Numeral
imports IntDef Datatype
-files "../Tools/numeral_syntax.ML"
+uses "../Tools/numeral_syntax.ML"
begin
text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
--- a/src/HOL/Integ/Presburger.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Integ/Presburger.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
theory Presburger
imports NatSimprocs SetInterval
-files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
+uses ("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/Isar_examples/BasicLogic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Basic logical reasoning *}
-theory BasicLogic = Main:
+theory BasicLogic imports Main begin
subsection {* Pure backward reasoning *}
--- a/src/HOL/Isar_examples/Cantor.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Cantor's Theorem *}
-theory Cantor = Main:
+theory Cantor imports Main begin
text_raw {*
\footnote{This is an Isar version of the final example of the
--- a/src/HOL/Isar_examples/Drinker.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Drinker.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The Drinker's Principle *}
-theory Drinker = Main:
+theory Drinker imports Main begin
text {*
Two parts of de-Morgan's law -- one intuitionistic and one classical:
--- a/src/HOL/Isar_examples/ExprCompiler.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Correctness of a simple expression compiler *}
-theory ExprCompiler = Main:
+theory ExprCompiler imports Main begin
text {*
This is a (rather trivial) example of program verification. We model
--- a/src/HOL/Isar_examples/Fibonacci.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Fri Jun 17 16:12:49 2005 +0200
@@ -15,7 +15,7 @@
header {* Fib and Gcd commute *}
-theory Fibonacci = Primes:
+theory Fibonacci imports Primes begin
text_raw {*
\footnote{Isar version by Gertrud Bauer. Original tactic script by
--- a/src/HOL/Isar_examples/Group.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Group.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Basic group theory *}
-theory Group = Main:
+theory Group imports Main begin
subsection {* Groups and calculational reasoning *}
--- a/src/HOL/Isar_examples/Hoare.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,8 +7,8 @@
header {* Hoare Logic *}
-theory Hoare = Main
-files ("~~/src/HOL/Hoare/hoare.ML"):
+theory Hoare imports Main
+uses ("~~/src/HOL/Hoare/hoare.ML") begin
subsection {* Abstract syntax and semantics *}
--- a/src/HOL/Isar_examples/HoareEx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* Using Hoare Logic *}
-theory HoareEx = Hoare:
+theory HoareEx imports Hoare begin
subsection {* State spaces *}
--- a/src/HOL/Isar_examples/KnasterTarski.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
-theory KnasterTarski = Main:
+theory KnasterTarski imports Main begin
subsection {* Prose version *}
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* The Mutilated Checker Board Problem *}
-theory MutilatedCheckerboard = Main:
+theory MutilatedCheckerboard imports Main begin
text {*
The Mutilated Checker Board Problem, formalized inductively. See
--- a/src/HOL/Isar_examples/NestedDatatype.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/NestedDatatype.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* Nested datatypes *}
-theory NestedDatatype = Main:
+theory NestedDatatype imports Main begin
subsection {* Terms and substitution *}
--- a/src/HOL/Isar_examples/Peirce.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Peirce's Law *}
-theory Peirce = Main:
+theory Peirce imports Main begin
text {*
We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is
--- a/src/HOL/Isar_examples/Puzzle.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* An old chestnut *}
-theory Puzzle = Main:
+theory Puzzle imports Main begin
text_raw {*
\footnote{A question from ``Bundeswettbewerb Mathematik''. Original
--- a/src/HOL/Lambda/Commutation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/Commutation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Abstract commutation and confluence notions *}
-theory Commutation = Main:
+theory Commutation imports Main begin
subsection {* Basic definitions *}
--- a/src/HOL/Lambda/Eta.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/Eta.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Eta-reduction *}
-theory Eta = ParRed:
+theory Eta imports ParRed begin
subsection {* Definition of eta-reduction and relatives *}
--- a/src/HOL/Lambda/InductTermi.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/InductTermi.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header {* Inductive characterization of terminating lambda terms *}
-theory InductTermi = ListBeta:
+theory InductTermi imports ListBeta begin
subsection {* Terminating lambda terms *}
--- a/src/HOL/Lambda/Lambda.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/Lambda.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Basic definitions of Lambda-calculus *}
-theory Lambda = Main:
+theory Lambda imports Main begin
subsection {* Lambda-terms in de Bruijn notation and substitution *}
--- a/src/HOL/Lambda/ListApplication.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Application of a term to a list of terms *}
-theory ListApplication = Lambda:
+theory ListApplication imports Lambda begin
syntax
"_list_application" :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150)
--- a/src/HOL/Lambda/ListBeta.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Lifting beta-reduction to lists *}
-theory ListBeta = ListApplication + ListOrder:
+theory ListBeta imports ListApplication ListOrder begin
text {*
Lifting beta-reduction to lists of terms, reducing exactly one element.
--- a/src/HOL/Lambda/ListOrder.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Lifting an order to lists of elements *}
-theory ListOrder = Accessible_Part:
+theory ListOrder imports Accessible_Part begin
text {*
Lifting an order to lists of elements, relating exactly one
--- a/src/HOL/Lambda/ParRed.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/ParRed.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header {* Parallel reduction and a complete developments *}
-theory ParRed = Lambda + Commutation:
+theory ParRed imports Lambda Commutation begin
subsection {* Parallel reduction *}
--- a/src/HOL/Lambda/StrongNorm.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/StrongNorm.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Strong normalization for simply-typed lambda calculus *}
-theory StrongNorm = Type + InductTermi:
+theory StrongNorm imports Type InductTermi begin
text {*
Formalization by Stefan Berghofer. Partly based on a paper proof by
--- a/src/HOL/Lambda/Type.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/Type.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Simply-typed lambda terms *}
-theory Type = ListApplication:
+theory Type imports ListApplication begin
subsection {* Environments *}
--- a/src/HOL/Lambda/WeakNorm.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Weak normalization for simply-typed lambda calculus *}
-theory WeakNorm = Type:
+theory WeakNorm imports Type begin
text {*
Formalization by Stefan Berghofer. Partly based on a paper proof by
--- a/src/HOL/Lattice/Bounds.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lattice/Bounds.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Bounds *}
-theory Bounds = Orders:
+theory Bounds imports Orders begin
subsection {* Infimum and supremum *}
--- a/src/HOL/Lattice/CompleteLattice.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Complete lattices *}
-theory CompleteLattice = Lattice:
+theory CompleteLattice imports Lattice begin
subsection {* Complete lattice operations *}
--- a/src/HOL/Lattice/Lattice.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lattice/Lattice.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Lattices *}
-theory Lattice = Bounds:
+theory Lattice imports Bounds begin
subsection {* Lattice operations *}
--- a/src/HOL/Lattice/Orders.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Lattice/Orders.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Orders *}
-theory Orders = Main:
+theory Orders imports Main begin
subsection {* Ordered structures *}
--- a/src/HOL/Library/Word.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Library/Word.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Word
imports Main
-files "word_setup.ML"
+uses "word_setup.ML"
begin
subsection {* Auxilary Lemmas *}
--- a/src/HOL/Matrix/MatrixGeneral.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Steven Obua
*)
-theory MatrixGeneral = Main:
+theory MatrixGeneral imports Main begin
types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"
--- a/src/HOL/Matrix/SparseMatrix.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory SparseMatrix = Matrix:
+theory SparseMatrix imports Matrix begin
types
'a spvec = "(nat * 'a) list"
--- a/src/HOL/MicroJava/BV/Altern.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Altern.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
used in compiler type correctness proof *)
-theory Altern = BVSpec:
+theory Altern imports BVSpec begin
constdefs
--- a/src/HOL/MicroJava/BV/BVExample.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
-theory BVExample = JVMListExample + BVSpecTypeSafe + JVM:
+theory BVExample imports JVMListExample BVSpecTypeSafe JVM begin
text {*
This theory shows type correctness of the example program in section
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* \isaheader{Welltyped Programs produce no Type Errors} *}
-theory BVNoTypeError = JVMDefensive + BVSpecTypeSafe:
+theory BVNoTypeError imports JVMDefensive BVSpecTypeSafe begin
text {*
Some simple lemmas about the type testing functions of the
--- a/src/HOL/MicroJava/BV/BVSpec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
-theory BVSpec = Effect:
+theory BVSpec imports Effect begin
text {*
This theory contains a specification of the BV. The specification
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
-theory BVSpecTypeSafe = Correct:
+theory BVSpecTypeSafe imports Correct begin
text {*
This theory contains proof that the specification of the bytecode
--- a/src/HOL/MicroJava/BV/Correct.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header {* \isaheader{BV Type Safety Invariant} *}
-theory Correct = BVSpec + JVMExec:
+theory Correct imports BVSpec JVMExec begin
constdefs
approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
--- a/src/HOL/MicroJava/BV/EffectMono.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Monotonicity of eff and app} *}
-theory EffectMono = Effect:
+theory EffectMono imports Effect begin
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
--- a/src/HOL/MicroJava/BV/Err.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* \isaheader{The Error Type} *}
-theory Err = Semilat:
+theory Err imports Semilat begin
datatype 'a err = Err | OK 'a
--- a/src/HOL/MicroJava/BV/JType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{The Java Type System as Semilattice} *}
-theory JType = WellForm + Err:
+theory JType imports WellForm Err begin
constdefs
super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname"
--- a/src/HOL/MicroJava/BV/JVM.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
-theory JVM = Kildall + Typing_Framework_JVM:
+theory JVM imports Kildall Typing_Framework_JVM begin
constdefs
--- a/src/HOL/MicroJava/BV/JVMType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* \isaheader{The JVM Type System as Semilattice} *}
-theory JVMType = Opt + Product + Listn + JType:
+theory JVMType imports Opt Product Listn JType begin
types
locvars_type = "ty err list"
--- a/src/HOL/MicroJava/BV/Kildall.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
-theory Kildall = SemilatAlg + While_Combinator:
+theory Kildall imports SemilatAlg While_Combinator begin
consts
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Completeness of the LBV} *}
-theory LBVComplete = LBVSpec + Typing_Framework:
+theory LBVComplete imports LBVSpec Typing_Framework begin
constdefs
is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool"
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Correctness of the LBV} *}
-theory LBVCorrect = LBVSpec + Typing_Framework:
+theory LBVCorrect imports LBVSpec Typing_Framework begin
locale (open) lbvs = lbv +
fixes s0 :: 'a ("s\<^sub>0")
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
-theory LBVJVM = LBVCorrect + LBVComplete + Typing_Framework_JVM:
+theory LBVJVM imports LBVCorrect LBVComplete Typing_Framework_JVM begin
types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> state list"
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{The Lightweight Bytecode Verifier} *}
-theory LBVSpec = SemilatAlg + Opt:
+theory LBVSpec imports SemilatAlg Opt begin
types
's certificate = "'s list"
--- a/src/HOL/MicroJava/BV/Listn.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* \isaheader{Fixed Length Lists} *}
-theory Listn = Err:
+theory Listn imports Err begin
constdefs
--- a/src/HOL/MicroJava/BV/Opt.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Opt.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* \isaheader{More about Options} *}
-theory Opt = Err:
+theory Opt imports Err begin
constdefs
le :: "'a ord \<Rightarrow> 'a option ord"
--- a/src/HOL/MicroJava/BV/Product.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Product.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* \isaheader{Products as Semilattices} *}
-theory Product = Err:
+theory Product imports Err begin
constdefs
le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
--- a/src/HOL/MicroJava/BV/Semilat.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
\isaheader{Semilattices}
*}
-theory Semilat = While_Combinator:
+theory Semilat imports While_Combinator begin
types 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{More on Semilattices} *}
-theory SemilatAlg = Typing_Framework + Product:
+theory SemilatAlg imports Typing_Framework Product begin
constdefs
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Typing and Dataflow Analysis Framework} *}
-theory Typing_Framework = Listn:
+theory Typing_Framework imports Listn begin
text {*
The relationship between dataflow analysis and a welltyped-instruction predicate.
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
-theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec:
+theory Typing_Framework_JVM imports Typing_Framework_err JVMType EffectMono BVSpec begin
constdefs
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}
-theory Typing_Framework_err = Typing_Framework + SemilatAlg:
+theory Typing_Framework_err imports Typing_Framework SemilatAlg begin
constdefs
--- a/src/HOL/MicroJava/Comp/Index.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
(* Index of variable in list of parameter names and local variables *)
-theory Index = AuxLemmas + DefsComp:
+theory Index imports AuxLemmas DefsComp begin
(*indexing a variable name among all variable declarations in a method body*)
constdefs
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
(* Lemmas for compiler correctness proof *)
-theory LemmasComp = TranslComp:
+theory LemmasComp imports TranslComp begin
declare split_paired_All [simp del]
--- a/src/HOL/MicroJava/Comp/NatCanonify.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/Comp/NatCanonify.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Martin Strecker
*)
-theory NatCanonify = Main:
+theory NatCanonify imports Main begin
(************************************************************************)
(* Canonizer for converting nat to int *)
--- a/src/HOL/MicroJava/Comp/TranslComp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/Comp/TranslComp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
(* Compiling MicroJava into MicroJVM -- Translation functions *)
-theory TranslComp = TranslCompTp:
+theory TranslComp imports TranslCompTp begin
(* parameter java_mb only serves to define function index later *)
--- a/src/HOL/MicroJava/Comp/TypeInf.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
*)
(* Exact position in theory hierarchy still to be determined *)
-theory TypeInf = WellType:
+theory TypeInf imports WellType begin
--- a/src/HOL/MicroJava/J/Conform.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
-theory Conform = State + WellType + Exceptions:
+theory Conform imports State WellType Exceptions begin
types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
--- a/src/HOL/MicroJava/J/Decl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Class Declarations and Programs} *}
-theory Decl = Type:
+theory Decl imports Type begin
types
fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)"
--- a/src/HOL/MicroJava/J/Eval.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Operational Evaluation (big step) Semantics} *}
-theory Eval = State + WellType:
+theory Eval imports State WellType begin
-- "Auxiliary notions"
--- a/src/HOL/MicroJava/J/Example.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Example MicroJava Program} *}
-theory Example = SystemClasses + Eval:
+theory Example imports SystemClasses Eval begin
text {*
The following example MicroJava program includes:
--- a/src/HOL/MicroJava/J/Exceptions.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 2002 Technische Universitaet Muenchen
*)
-theory Exceptions = State:
+theory Exceptions imports State begin
text {* a new, blank object with default values in all fields: *}
constdefs
--- a/src/HOL/MicroJava/J/JBasis.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
\isaheader{Some Auxiliary Definitions}
*}
-theory JBasis = Main:
+theory JBasis imports Main begin
lemmas [simp] = Let_def
--- a/src/HOL/MicroJava/J/JListExample.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* \isaheader{Example for generating executable code from Java semantics} *}
-theory JListExample = Eval + SystemClasses:
+theory JListExample imports Eval SystemClasses begin
ML {* Syntax.ambiguity_level := 100000 *}
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Type Safety Proof} *}
-theory JTypeSafe = Eval + Conform:
+theory JTypeSafe imports Eval Conform begin
declare split_beta [simp]
--- a/src/HOL/MicroJava/J/State.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Program State} *}
-theory State = TypeRel + Value:
+theory State imports TypeRel Value begin
types
fields_ = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value"
--- a/src/HOL/MicroJava/J/SystemClasses.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{System Classes} *}
-theory SystemClasses = Decl:
+theory SystemClasses imports Decl begin
text {*
This theory provides definitions for the @{text Object} class,
--- a/src/HOL/MicroJava/J/Term.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Expressions and Statements} *}
-theory Term = Value:
+theory Term imports Value begin
datatype binop = Eq | Add -- "function codes for binary operation"
--- a/src/HOL/MicroJava/J/Type.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Java types} *}
-theory Type = JBasis:
+theory Type imports JBasis begin
typedecl cnam
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Relations between Java Types} *}
-theory TypeRel = Decl:
+theory TypeRel imports Decl begin
consts
subcls1 :: "'c prog => (cname \<times> cname) set" -- "subclass"
--- a/src/HOL/MicroJava/J/Value.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Java Values} *}
-theory Value = Type:
+theory Value imports Type begin
typedecl loc_ -- "locations, i.e. abstract references on objects"
--- a/src/HOL/MicroJava/J/WellForm.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Well-formedness of Java programs} *}
-theory WellForm = TypeRel + SystemClasses:
+theory WellForm imports TypeRel SystemClasses begin
text {*
for static checks on expressions and statements, see WellType.
--- a/src/HOL/MicroJava/J/WellType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Well-typedness Constraints} *}
-theory WellType = Term + WellForm:
+theory WellType imports Term WellForm begin
text {*
the formulation of well-typedness of method calls given below (as well as
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* \isaheader{A Defensive JVM} *}
-theory JVMDefensive = JVMExec:
+theory JVMDefensive imports JVMExec begin
text {*
Extend the state space by one element indicating a type error (or
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Exception handling in the JVM} *}
-theory JVMExceptions = JVMInstructions:
+theory JVMExceptions imports JVMInstructions begin
constdefs
match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool"
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* \isaheader{Program Execution in the JVM} *}
-theory JVMExec = JVMExecInstr + JVMExceptions:
+theory JVMExec imports JVMExecInstr JVMExceptions begin
consts
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* \isaheader{JVM Instruction Semantics} *}
-theory JVMExecInstr = JVMInstructions + JVMState:
+theory JVMExecInstr imports JVMInstructions JVMState begin
consts
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* \isaheader{Instructions of the JVM} *}
-theory JVMInstructions = JVMState:
+theory JVMInstructions imports JVMState begin
datatype
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
-theory JVMListExample = SystemClasses + JVMExec:
+theory JVMListExample imports SystemClasses JVMExec begin
consts
list_nam :: cnam
--- a/src/HOL/NanoJava/AxSem.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Axiomatic Semantics"
-theory AxSem = State:
+theory AxSem imports State begin
types assn = "state => bool"
vassn = "val => assn"
--- a/src/HOL/NanoJava/Decl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/Decl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Types, class Declarations, and whole programs"
-theory Decl = Term:
+theory Decl imports Term begin
datatype ty
= NT --{* null type *}
--- a/src/HOL/NanoJava/Equivalence.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Equivalence of Operational and Axiomatic Semantics"
-theory Equivalence = OpSem + AxSem:
+theory Equivalence imports OpSem AxSem begin
subsection "Validity"
--- a/src/HOL/NanoJava/Example.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/Example.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Example"
-theory Example = Equivalence:
+theory Example imports Equivalence begin
text {*
--- a/src/HOL/NanoJava/OpSem.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/OpSem.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Operational Evaluation Semantics"
-theory OpSem = State:
+theory OpSem imports State begin
consts
exec :: "(state \<times> stmt \<times> nat \<times> state) set"
--- a/src/HOL/NanoJava/State.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/State.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Program State"
-theory State = TypeRel:
+theory State imports TypeRel begin
constdefs
--- a/src/HOL/NanoJava/Term.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/Term.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Statements and expression emulations"
-theory Term = Main:
+theory Term imports Main begin
typedecl cname --{* class name *}
typedecl mname --{* method name *}
--- a/src/HOL/NanoJava/TypeRel.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Type relations"
-theory TypeRel = Decl:
+theory TypeRel imports Decl begin
consts
widen :: "(ty \<times> ty ) set" --{* widening *}
--- a/src/HOL/NatArith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NatArith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory NatArith
imports Nat
-files "arith_data.ML"
+uses "arith_data.ML"
begin
setup arith_setup
--- a/src/HOL/NumberTheory/BijectionRel.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Bijections between sets *}
-theory BijectionRel = Main:
+theory BijectionRel imports Main begin
text {*
Inductive definitions of bijections between two different sets and
--- a/src/HOL/NumberTheory/Chinese.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* The Chinese Remainder Theorem *}
-theory Chinese = IntPrimes:
+theory Chinese imports IntPrimes begin
text {*
The Chinese Remainder Theorem for an arbitrary finite number of
--- a/src/HOL/NumberTheory/Euler.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Euler.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Euler's criterion *}
-theory Euler = Residues + EvenOdd:;
+theory Euler imports Residues EvenOdd begin;
constdefs
MultInvPair :: "int => int => int => int set"
--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header {* Fermat's Little Theorem extended to Euler's Totient function *}
-theory EulerFermat = BijectionRel + IntFact:
+theory EulerFermat imports BijectionRel IntFact begin
text {*
Fermat's Little Theorem extended to Euler's Totient function. More
--- a/src/HOL/NumberTheory/EvenOdd.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Parity: Even and Odd Integers*}
-theory EvenOdd = Int2:;
+theory EvenOdd imports Int2 begin;
text{*Note. This theory is being revised. See the web page
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
--- a/src/HOL/NumberTheory/Factorization.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
-theory Factorization = Primes + Permutation:
+theory Factorization imports Primes Permutation begin
subsection {* Definitions *}
--- a/src/HOL/NumberTheory/Fib.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The Fibonacci function *}
-theory Fib = Primes:
+theory Fib imports Primes begin
text {*
Fibonacci numbers: proofs of laws taken from:
--- a/src/HOL/NumberTheory/Gauss.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Gauss' Lemma *}
-theory Gauss = Euler:;
+theory Gauss imports Euler begin;
locale GAUSS =
fixes p :: "int"
--- a/src/HOL/NumberTheory/Int2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Int2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Integers: Divisibility and Congruences*}
-theory Int2 = Finite2 + WilsonRuss:;
+theory Int2 imports Finite2 WilsonRuss begin;
text{*Note. This theory is being revised. See the web page
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
--- a/src/HOL/NumberTheory/IntFact.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Factorial on integers *}
-theory IntFact = IntPrimes:
+theory IntFact imports IntPrimes begin
text {*
Factorial on integers and recursively defined set including all
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header {* Divisibility and prime numbers (on integers) *}
-theory IntPrimes = Primes:
+theory IntPrimes imports Primes begin
text {*
The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
--- a/src/HOL/NumberTheory/Residues.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/Residues.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Residue Sets *}
-theory Residues = Int2:;
+theory Residues imports Int2 begin;
text{*Note. This theory is being revised. See the web page
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
--- a/src/HOL/NumberTheory/WilsonBij.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Wilson's Theorem using a more abstract approach *}
-theory WilsonBij = BijectionRel + IntFact:
+theory WilsonBij imports BijectionRel IntFact begin
text {*
Wilson's Theorem using a more ``abstract'' approach based on
--- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header {* Wilson's Theorem according to Russinoff *}
-theory WilsonRuss = EulerFermat:
+theory WilsonRuss imports EulerFermat begin
text {*
Wilson's Theorem following quite closely Russinoff's approach
--- a/src/HOL/OrderedGroup.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/OrderedGroup.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory OrderedGroup
imports Inductive LOrder
-files "../Provers/Arith/abel_cancel.ML"
+uses "../Provers/Arith/abel_cancel.ML"
begin
text {*
--- a/src/HOL/Orderings.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Orderings.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
theory Orderings
imports Lattice_Locales
-files ("antisym_setup.ML")
+uses ("antisym_setup.ML")
begin
subsection {* Order signatures and orders *}
--- a/src/HOL/Presburger.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Presburger.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
theory Presburger
imports NatSimprocs SetInterval
-files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
+uses ("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 Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Product_Type.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
theory Product_Type
imports Fun
-files ("Tools/split_rule.ML")
+uses ("Tools/split_rule.ML")
begin
subsection {* Unit *}
--- a/src/HOL/Real/HahnBanach/Bounds.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Bounds *}
-theory Bounds = Main + Real:
+theory Bounds imports Main Real begin
locale lub =
fixes A and x
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The norm of a function *}
-theory FunctionNorm = NormedSpace + FunctionOrder:
+theory FunctionNorm imports NormedSpace FunctionOrder begin
subsection {* Continuous linear forms*}
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* An order on functions *}
-theory FunctionOrder = Subspace + Linearform:
+theory FunctionOrder imports Subspace Linearform begin
subsection {* The graph of a function *}
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The Hahn-Banach Theorem *}
-theory HahnBanach = HahnBanachLemmas:
+theory HahnBanach imports HahnBanachLemmas begin
text {*
We present the proof of two different versions of the Hahn-Banach
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Extending non-maximal functions *}
-theory HahnBanachExtLemmas = FunctionNorm:
+theory HahnBanachExtLemmas imports FunctionNorm begin
text {*
In this section the following context is presumed. Let @{text E} be
--- a/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
(*<*)
-theory HahnBanachLemmas = HahnBanachSupLemmas + HahnBanachExtLemmas:
+theory HahnBanachLemmas imports HahnBanachSupLemmas HahnBanachExtLemmas begin
end
(*>*)
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The supremum w.r.t.~the function order *}
-theory HahnBanachSupLemmas = FunctionNorm + ZornLemma:
+theory HahnBanachSupLemmas imports FunctionNorm ZornLemma begin
text {*
This section contains some lemmas that will be used in the proof of
--- a/src/HOL/Real/HahnBanach/Linearform.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Linearforms *}
-theory Linearform = VectorSpace:
+theory Linearform imports VectorSpace begin
text {*
A \emph{linear form} is a function on a vector space into the reals
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Normed vector spaces *}
-theory NormedSpace = Subspace:
+theory NormedSpace imports Subspace begin
subsection {* Quasinorms *}
--- a/src/HOL/Real/HahnBanach/Subspace.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Subspaces *}
-theory Subspace = VectorSpace:
+theory Subspace imports VectorSpace begin
subsection {* Definition *}
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Vector spaces *}
-theory VectorSpace = Real + Bounds + Zorn:
+theory VectorSpace imports Real Bounds Zorn begin
subsection {* Signature *}
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Zorn's Lemma *}
-theory ZornLemma = Zorn:
+theory ZornLemma imports Zorn begin
text {*
Zorn's Lemmas states: if every linear ordered subset of an ordered
--- a/src/HOL/Real/Rational.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/Rational.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Rational
imports Quotient
-files ("rat_arith.ML")
+uses ("rat_arith.ML")
begin
subsection {* Fractions *}
--- a/src/HOL/Real/RealDef.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Real/RealDef.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
theory RealDef
imports PReal
-files ("real_arith.ML")
+uses ("real_arith.ML")
begin
constdefs
--- a/src/HOL/Recdef.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Recdef.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Recdef
imports Wellfounded_Relations Datatype
-files
+uses
("../TFL/casesplit.ML")
("../TFL/utils.ML")
("../TFL/usyntax.ML")
--- a/src/HOL/Reconstruction.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Reconstruction.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
theory Reconstruction
imports Hilbert_Choice Map Infinite_Set Extraction
- files "Tools/res_lib.ML"
+ uses "Tools/res_lib.ML"
"Tools/res_clause.ML"
"Tools/res_skolem_function.ML"
"Tools/res_axioms.ML"
--- a/src/HOL/Record.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Record.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
theory Record
imports Product_Type
-files ("Tools/record_package.ML")
+uses ("Tools/record_package.ML")
begin
ML {*
--- a/src/HOL/Refute.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Refute.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
theory Refute
imports Map
-files "Tools/prop_logic.ML"
+uses "Tools/prop_logic.ML"
"Tools/sat_solver.ML"
"Tools/refute.ML"
"Tools/refute_isar.ML"
--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The SET Cardholder Registration Protocol*}
-theory Cardholder_Registration = PublicSET:
+theory Cardholder_Registration imports PublicSET begin
text{*Note: nonces seem to consist of 20 bytes. That includes both freshness
challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
--- a/src/HOL/SET-Protocol/EventSET.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/SET-Protocol/EventSET.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*Theory of Events for SET*}
-theory EventSET = MessageSET:
+theory EventSET imports MessageSET begin
text{*The Root Certification Authority*}
syntax RCA :: agent
--- a/src/HOL/SET-Protocol/Merchant_Registration.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/SET-Protocol/Merchant_Registration.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*The SET Merchant Registration Protocol*}
-theory Merchant_Registration = PublicSET:
+theory Merchant_Registration imports PublicSET begin
text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not
needed: no session key encrypts another. Instead we
--- a/src/HOL/SET-Protocol/MessageSET.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*The Message Theory, Modified for SET*}
-theory MessageSET = NatPair:
+theory MessageSET imports NatPair begin
subsection{*General Lemmas*}
--- a/src/HOL/SET-Protocol/PublicSET.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*The Public-Key Theory, Modified for SET*}
-theory PublicSET = EventSET:
+theory PublicSET imports EventSET begin
subsection{*Symmetric and Asymmetric Keys*}
--- a/src/HOL/SET-Protocol/Purchase.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/SET-Protocol/Purchase.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*Purchase Phase of SET*}
-theory Purchase = PublicSET:
+theory Purchase imports PublicSET begin
text{*
Note: nonces seem to consist of 20 bytes. That includes both freshness
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
Basic declarations for the RPC-memory example.
*)
-theory RPCMemoryParams = Main:
+theory RPCMemoryParams imports Main begin
types
bit = "bool" (* Signal wires for the procedure interface.
--- a/src/HOL/Transitive_Closure.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
theory Transitive_Closure
imports Inductive
-files ("../Provers/trancl.ML")
+uses ("../Provers/trancl.ML")
begin
text {*
--- a/src/HOL/Typedef.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Typedef.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Typedef
imports Set
-files ("Tools/typedef_package.ML")
+uses ("Tools/typedef_package.ML")
begin
locale type_definition =
--- a/src/HOL/UNITY/Comp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -15,7 +15,7 @@
header{*Composition: Basic Primitives*}
-theory Comp = Union:
+theory Comp imports Union begin
instance program :: (type) ord ..
--- a/src/HOL/UNITY/Comp/AllocBase.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Common Declarations for Chandy and Charpentier's Allocator*}
-theory AllocBase = UNITY_Main:
+theory AllocBase imports UNITY_Main begin
consts
NbT :: nat (*Number of tokens in system*)
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Implementation of a multiple-client allocator from a single-client allocator*}
-theory AllocImpl = AllocBase + Follows + PPROD:
+theory AllocImpl imports AllocBase Follows PPROD begin
(** State definitions. OUTPUT variables are locals **)
--- a/src/HOL/UNITY/Comp/Client.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Distributed Resource Management System: the Client*}
-theory Client = Rename + AllocBase:
+theory Client imports Rename AllocBase begin
types
tokbag = nat --{*tokbags could be multisets...or any ordered type?*}
--- a/src/HOL/UNITY/Comp/Counter.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*A Family of Similar Counters: Original Version*}
-theory Counter = UNITY_Main:
+theory Counter imports UNITY_Main begin
(* Variables are names *)
datatype name = C | c nat
--- a/src/HOL/UNITY/Comp/Counterc.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy Fri Jun 17 16:12:49 2005 +0200
@@ -13,7 +13,7 @@
header{*A Family of Similar Counters: Version with Compatibility*}
-theory Counterc = UNITY_Main:
+theory Counterc imports UNITY_Main begin
typedecl state
arities state :: type
--- a/src/HOL/UNITY/Comp/Handshake.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)
-theory Handshake = UNITY_Main:
+theory Handshake imports UNITY_Main begin
record state =
BB :: bool
--- a/src/HOL/UNITY/Comp/Priority.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The priority system*}
-theory Priority = PriorityAux:
+theory Priority imports PriorityAux begin
text{*From Charpentier and Chandy,
Examples of Program Composition Illustrating the Use of Universal Properties
--- a/src/HOL/UNITY/Comp/Progress.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/Progress.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Progress Set Examples*}
-theory Progress = UNITY_Main:
+theory Progress imports UNITY_Main begin
subsection {*The Composition of Two Single-Assignment Programs*}
text{*Thesis Section 4.4.2*}
--- a/src/HOL/UNITY/Comp/TimerArray.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
A trivial example of reasoning about an array of processes
*)
-theory TimerArray = UNITY_Main:
+theory TimerArray imports UNITY_Main begin
types 'a state = "nat * 'a" (*second component allows new variables*)
--- a/src/HOL/UNITY/Constrains.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Constrains.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Weak Safety*}
-theory Constrains = UNITY:
+theory Constrains imports UNITY begin
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
--- a/src/HOL/UNITY/Detects.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Detects.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*The Detects Relation*}
-theory Detects = FP + SubstAx:
+theory Detects imports FP SubstAx begin
consts
op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60)
--- a/src/HOL/UNITY/ELT.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/ELT.thy Fri Jun 17 16:12:49 2005 +0200
@@ -24,7 +24,7 @@
header{*Progress Under Allowable Sets*}
-theory ELT = Project:
+theory ELT imports Project begin
consts
--- a/src/HOL/UNITY/Extend.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Extend.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header{*Extending State Sets*}
-theory Extend = Guar:
+theory Extend imports Guar begin
constdefs
--- a/src/HOL/UNITY/FP.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/FP.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Fixed Point of a Program*}
-theory FP = UNITY:
+theory FP imports UNITY begin
constdefs
--- a/src/HOL/UNITY/Follows.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Follows.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Follows Relation of Charpentier and Sivilotte*}
-theory Follows = SubstAx + ListOrder + Multiset:
+theory Follows imports SubstAx ListOrder Multiset begin
constdefs
--- a/src/HOL/UNITY/Guar.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Guar.thy Fri Jun 17 16:12:49 2005 +0200
@@ -18,7 +18,7 @@
header{*Guarantees Specifications*}
-theory Guar = Comp:
+theory Guar imports Comp begin
instance program :: (type) order
by (intro_classes,
--- a/src/HOL/UNITY/Lift_prog.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Replication of Components*}
-theory Lift_prog = Rename:
+theory Lift_prog imports Rename begin
constdefs
--- a/src/HOL/UNITY/ListOrder.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/ListOrder.thy Fri Jun 17 16:12:49 2005 +0200
@@ -15,7 +15,7 @@
header {*The Prefix Ordering on Lists*}
-theory ListOrder = Main:
+theory ListOrder imports Main begin
consts
genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
--- a/src/HOL/UNITY/PPROD.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/PPROD.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
Some dead wood here!
*)
-theory PPROD = Lift_prog:
+theory PPROD imports Lift_prog begin
constdefs
--- a/src/HOL/UNITY/ProgressSets.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
header{*Progress Sets*}
-theory ProgressSets = Transformers:
+theory ProgressSets imports Transformers begin
subsection {*Complete Lattices and the Operator @{term cl}*}
--- a/src/HOL/UNITY/Project.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Project.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header{*Projections of State Sets*}
-theory Project = Extend:
+theory Project imports Extend begin
constdefs
projecting :: "['c program => 'c set, 'a*'b => 'c,
--- a/src/HOL/UNITY/Rename.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Rename.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Renaming of State Sets*}
-theory Rename = Extend:
+theory Rename imports Extend begin
constdefs
--- a/src/HOL/UNITY/Simple/Channel.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Channel.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
*)
-theory Channel = UNITY_Main:
+theory Channel imports UNITY_Main begin
types state = "nat set"
--- a/src/HOL/UNITY/Simple/Common.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-theory Common = UNITY_Main:
+theory Common imports UNITY_Main begin
consts
ftime :: "nat=>nat"
--- a/src/HOL/UNITY/Simple/Deadlock.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Deadlock.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Misra, "A Logic for Concurrent Programming", 1994
*)
-theory Deadlock = UNITY:
+theory Deadlock imports UNITY begin
(*Trivial, two-process case*)
lemma "[| F \<in> (A \<inter> B) co A; F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)"
--- a/src/HOL/UNITY/Simple/Mutex.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)
-theory Mutex = UNITY_Main:
+theory Mutex imports UNITY_Main begin
record state =
p :: bool
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
-theory NSP_Bad = Public + UNITY_Main:
+theory NSP_Bad imports Public UNITY_Main begin
text{*This is the flawed version, vulnerable to Lowe's attack.
From page 260 of
--- a/src/HOL/UNITY/Simple/Network.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Network.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
*)
-theory Network = UNITY:
+theory Network imports UNITY begin
(*The state assigns a number to each process variable*)
--- a/src/HOL/UNITY/Simple/Reach.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
[this example took only four days!]
*)
-theory Reach = UNITY_Main:
+theory Reach imports UNITY_Main begin
typedecl vertex
--- a/src/HOL/UNITY/Simple/Reachability.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
*)
-theory Reachability = Detects + Reach:
+theory Reachability imports Detects Reach begin
types edge = "(vertex*vertex)"
--- a/src/HOL/UNITY/SubstAx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Weak Progress*}
-theory SubstAx = WFair + Constrains:
+theory SubstAx imports WFair Constrains begin
constdefs
Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60)
--- a/src/HOL/UNITY/Transformers.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Transformers.thy Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
header{*Predicate Transformers*}
-theory Transformers = Comp:
+theory Transformers imports Comp begin
subsection{*Defining the Predicate Transformers @{term wp},
@{term awp} and @{term wens}*}
--- a/src/HOL/UNITY/UNITY.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/UNITY.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header {*The Basic UNITY Theory*}
-theory UNITY = Main:
+theory UNITY imports Main begin
typedef (Program)
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
--- a/src/HOL/UNITY/UNITY_Main.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,8 +6,8 @@
header{*Comprehensive UNITY Theory*}
-theory UNITY_Main = Detects + PPROD + Follows + ProgressSets
-files "UNITY_tactics.ML":
+theory UNITY_Main imports Detects PPROD Follows ProgressSets
+uses "UNITY_tactics.ML" begin
method_setup safety = {*
Method.ctxt_args (fn ctxt =>
--- a/src/HOL/UNITY/Union.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/Union.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Unions of Programs*}
-theory Union = SubstAx + FP:
+theory Union imports SubstAx FP begin
constdefs
--- a/src/HOL/UNITY/WFair.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/UNITY/WFair.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header{*Progress*}
-theory WFair = UNITY:
+theory WFair imports UNITY begin
text{*The original version of this theory was based on weak fairness. (Thus,
the entire UNITY development embodied this assumption, until February 2003.)
--- a/src/HOL/Unix/Unix.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Unix/Unix.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Unix file-systems \label{sec:unix-file-system} *}
-theory Unix = Nested_Environment + List_Prefix:
+theory Unix imports Nested_Environment List_Prefix begin
text {*
We give a simple mathematical model of the basic structures
--- a/src/HOL/ex/Adder.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Adder.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{* Adder *}
-theory Adder = Main + Word:
+theory Adder imports Main Word begin
lemma [simp]: "bv_to_nat [b] = bitval b"
by (simp add: bv_to_nat_helper)
--- a/src/HOL/ex/Antiquote.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Antiquote.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Antiquotations *}
-theory Antiquote = Main:
+theory Antiquote imports Main begin
text {*
A simple example on quote / antiquote in higher-order abstract
--- a/src/HOL/ex/BT.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/BT.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* Binary trees *}
-theory BT = Main:
+theory BT imports Main begin
datatype 'a bt =
Lf
--- a/src/HOL/ex/BinEx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/BinEx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Binary arithmetic examples *}
-theory BinEx = Main:
+theory BinEx imports Main begin
subsection {* Regression Testing for Cancellation Simprocs *}
--- a/src/HOL/ex/CTL.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/CTL.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* CTL formulae *}
-theory CTL = Main:
+theory CTL imports Main begin
--- a/src/HOL/ex/Classical.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Classical.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Classical Predicate Calculus Problems*}
-theory Classical = Main:
+theory Classical imports Main begin
subsection{*Traditional Classical Reasoner*}
--- a/src/HOL/ex/Higher_Order_Logic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Foundations of HOL *}
-theory Higher_Order_Logic = CPure:
+theory Higher_Order_Logic imports CPure begin
text {*
The following theory development demonstrates Higher-Order Logic
--- a/src/HOL/ex/Hilbert_Classical.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Hilbert_Classical.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Hilbert's choice and classical logic *}
-theory Hilbert_Classical = Main:
+theory Hilbert_Classical imports Main begin
text {*
Derivation of the classical law of tertium-non-datur by means of
--- a/src/HOL/ex/InductiveInvariant.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory InductiveInvariant = Main:
+theory InductiveInvariant imports Main begin
(** Authors: Sava Krsti\'{c} and John Matthews **)
(** Date: Sep 12, 2003 **)
--- a/src/HOL/ex/InductiveInvariant_examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,4 +1,4 @@
-theory InductiveInvariant_examples = InductiveInvariant :
+theory InductiveInvariant_examples imports InductiveInvariant begin
(** Authors: Sava Krsti\'{c} and John Matthews **)
(** Date: Oct 17, 2003 **)
--- a/src/HOL/ex/Intuitionistic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Intuitionistic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
Taken from FOL/ex/int.ML
*)
-theory Intuitionistic = Main:
+theory Intuitionistic imports Main begin
(*Metatheorem (for PROPOSITIONAL formulae...):
--- a/src/HOL/ex/Lagrange.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Lagrange.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
The enterprising reader might consider proving all of Lagrange's theorem.
*)
-theory Lagrange = Main:
+theory Lagrange imports Main begin
constdefs sq :: "'a::times => 'a"
"sq x == x*x"
--- a/src/HOL/ex/Locales.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Locales.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Using locales in Isabelle/Isar *}
-theory Locales = Main:
+theory Locales imports Main begin
text_raw {*
\newcommand{\isasyminv}{\isasyminverse}
--- a/src/HOL/ex/MonoidGroup.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/MonoidGroup.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header {* Monoids and Groups *}
-theory MonoidGroup = Main:
+theory MonoidGroup imports Main begin
record 'a monoid_sig =
times :: "'a => 'a => 'a"
--- a/src/HOL/ex/Multiquote.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Multiquote.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Multiple nested quotations and anti-quotations *}
-theory Multiquote = Main:
+theory Multiquote imports Main begin
text {*
Multiple nested quotations and anti-quotations -- basically a
--- a/src/HOL/ex/NatSum.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/NatSum.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Summing natural numbers *}
-theory NatSum = Main:
+theory NatSum imports Main begin
text {*
Summing natural numbers, squares, cubes, etc.
--- a/src/HOL/ex/PER.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/PER.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Partial equivalence relations *}
-theory PER = Main:
+theory PER imports Main begin
text {*
Higher-order quotients are defined over partial equivalence
--- a/src/HOL/ex/PresburgerEx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/PresburgerEx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Some examples for Presburger Arithmetic
*)
-theory PresburgerEx = Main:
+theory PresburgerEx imports Main begin
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
by presburger
--- a/src/HOL/ex/Primrec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Primrec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header {* Primitive Recursive Functions *}
-theory Primrec = Main:
+theory Primrec imports Main begin
text {*
Proof adopted from
--- a/src/HOL/ex/Puzzle.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Puzzle.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
Proof due to Herbert Ehler
*)
-theory Puzzle = Main:
+theory Puzzle imports Main begin
consts f :: "nat => nat"
--- a/src/HOL/ex/Quickcheck_Examples.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Examples for the 'quickcheck' command *}
-theory Quickcheck_Examples = Main:
+theory Quickcheck_Examples imports Main begin
text {*
The 'quickcheck' command allows to find counterexamples by evaluating
--- a/src/HOL/ex/Recdefs.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Recdefs.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header {* Examples of recdef definitions *}
-theory Recdefs = Main:
+theory Recdefs imports Main begin
consts fact :: "nat => nat"
recdef fact less_than
--- a/src/HOL/ex/Records.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Records.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Using extensible records in HOL -- points and coloured points *}
-theory Records = Main:
+theory Records imports Main begin
subsection {* Points *}
--- a/src/HOL/ex/SVC_Oracle.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,8 +8,8 @@
Based upon the work of Søren T. Heilmann
*)
-theory SVC_Oracle = Main (** + Real??**)
-files "svc_funcs.ML":
+theory SVC_Oracle imports Main (** + Real??**)
+uses "svc_funcs.ML" begin
consts
(*reserved for the oracle*)
--- a/src/HOL/ex/StringEx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/StringEx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
header {* String examples *}
-theory StringEx = Main:
+theory StringEx imports Main begin
lemma "hd ''ABCD'' = CHR ''A''"
by simp
--- a/src/HOL/ex/Tarski.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Tarski.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The Full Theorem of Tarski *}
-theory Tarski = Main + FuncSet:
+theory Tarski imports Main FuncSet begin
text {*
Minimal version of lattice theory plus the full theorem of Tarski:
--- a/src/HOL/ex/Tuple.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/Tuple.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header {* Properly nested products *}
-theory Tuple = HOL:
+theory Tuple imports HOL begin
subsection {* Abstract syntax *}
--- a/src/HOL/ex/mesontest2.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/mesontest2.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,6 +1,6 @@
(*ID: $Id$*)
header {* Meson test cases *}
-theory mesontest2 = Main:
+theory mesontest2 imports Main begin
end
--- a/src/HOL/ex/set.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/set.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Set Theory examples: Cantor's Theorem, Schröder-Berstein Theorem, etc. *}
-theory set = Main:
+theory set imports Main begin
text{*
These two are cited in Benzmueller and Kohlhase's system description
--- a/src/HOLCF/Cfun.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/Cfun.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
theory Cfun
imports TypedefPcpo
-files ("cont_proc.ML")
+uses ("cont_proc.ML")
begin
defaultsort cpo
--- a/src/HOLCF/FOCUS/Fstreams.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
###TODO: integrate this with Fstream.*
*)
-theory Fstreams = Stream:
+theory Fstreams imports Stream begin
defaultsort type
--- a/src/HOLCF/Fixrec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/Fixrec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
theory Fixrec
imports Ssum One Up Fix
-files ("fixrec_package.ML")
+uses ("fixrec_package.ML")
begin
subsection {* Maybe monad type *}
--- a/src/HOLCF/IMP/Denotational.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/IMP/Denotational.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Denotational Semantics of Commands in HOLCF"
-theory Denotational = HOLCF + Natural:
+theory Denotational imports HOLCF Natural begin
subsection "Definition"
--- a/src/HOLCF/IMP/HoareEx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/IMP/HoareEx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header "Correctness of Hoare by Fixpoint Reasoning"
-theory HoareEx = Denotational:
+theory HoareEx imports Denotational begin
text {*
An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
--- a/src/HOLCF/ex/Dnat.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/ex/Dnat.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Theory for the domain of natural numbers dnat = one ++ dnat
*)
-theory Dnat = HOLCF:
+theory Dnat imports HOLCF begin
domain dnat = dzero | dsucc (dpred :: dnat)
--- a/src/HOLCF/ex/Stream.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOLCF/ex/Stream.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
General Stream domain.
*)
-theory Stream = HOLCF + Nat_Infinity:
+theory Stream imports HOLCF Nat_Infinity begin
domain 'a stream = "&&" (ft::'a) (lazy rt::"'a stream") (infixr 65)
--- a/src/ZF/AC.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*The Axiom of Choice*}
-theory AC = Main:
+theory AC imports Main begin
text{*This definition comes from Halmos (1960), page 59.*}
axioms AC: "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
--- a/src/ZF/AC/AC15_WO6.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC15_WO6.thy Fri Jun 17 16:12:49 2005 +0200
@@ -20,7 +20,7 @@
Rubin & Rubin do.
*)
-theory AC15_WO6 = HH + Cardinal_aux:
+theory AC15_WO6 imports HH Cardinal_aux begin
(* ********************************************************************** *)
--- a/src/ZF/AC/AC16_WO4.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC16_WO4.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Tidied (using locales) by LCP
*)
-theory AC16_WO4 = AC16_lemmas:
+theory AC16_WO4 imports AC16_lemmas begin
(* ********************************************************************** *)
(* The case of finite set *)
--- a/src/ZF/AC/AC16_lemmas.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC16_lemmas.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Lemmas used in the proofs concerning AC16
*)
-theory AC16_lemmas = AC_Equiv + Hartog + Cardinal_aux:
+theory AC16_lemmas imports AC_Equiv Hartog Cardinal_aux begin
lemma cons_Diff_eq: "a\<notin>A ==> cons(a,A)-{a}=A"
by fast
--- a/src/ZF/AC/AC17_AC1.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC17_AC1.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
to AC0 and AC1.
*)
-theory AC17_AC1 = HH:
+theory AC17_AC1 imports HH begin
(** AC0 is equivalent to AC1.
--- a/src/ZF/AC/AC18_AC19.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC18_AC19.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
The proof of AC1 ==> AC18 ==> AC19 ==> AC1
*)
-theory AC18_AC19 = AC_Equiv:
+theory AC18_AC19 imports AC_Equiv begin
constdefs
uu :: "i => i"
--- a/src/ZF/AC/AC7_AC9.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC7_AC9.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
instances of AC.
*)
-theory AC7_AC9 = AC_Equiv:
+theory AC7_AC9 imports AC_Equiv begin
(* ********************************************************************** *)
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *)
--- a/src/ZF/AC/AC_Equiv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -12,7 +12,7 @@
but slightly changed.
*)
-theory AC_Equiv = Main: (*obviously not Main_ZFC*)
+theory AC_Equiv imports Main begin (*obviously not Main_ZFC*)
constdefs
--- a/src/ZF/AC/Cardinal_aux.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/Cardinal_aux.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Auxiliary lemmas concerning cardinalities
*)
-theory Cardinal_aux = AC_Equiv:
+theory Cardinal_aux imports AC_Equiv begin
lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m"
apply (rule not_emptyE, assumption)
--- a/src/ZF/AC/DC.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/DC.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
The proofs concerning the Axiom of Dependent Choice
*)
-theory DC = AC_Equiv + Hartog + Cardinal_aux:
+theory DC imports AC_Equiv Hartog Cardinal_aux begin
lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a"
apply (unfold lepoll_def)
--- a/src/ZF/AC/HH.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/HH.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
AC15 ==> WO6
*)
-theory HH = AC_Equiv + Hartog:
+theory HH imports AC_Equiv Hartog begin
constdefs
--- a/src/ZF/AC/Hartog.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/Hartog.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Hartog's function.
*)
-theory Hartog = AC_Equiv:
+theory Hartog imports AC_Equiv begin
constdefs
Hartog :: "i => i"
--- a/src/ZF/AC/WO1_AC.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/WO1_AC.thy Fri Jun 17 16:12:49 2005 +0200
@@ -25,7 +25,7 @@
*)
-theory WO1_AC = AC_Equiv:
+theory WO1_AC imports AC_Equiv begin
(* ********************************************************************** *)
(* WO1 ==> AC1 *)
--- a/src/ZF/AC/WO1_WO7.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/WO1_WO7.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
Also, WO1 <-> WO8
*)
-theory WO1_WO7 = AC_Equiv:
+theory WO1_WO7 imports AC_Equiv begin
constdefs
LEMMA :: o
--- a/src/ZF/AC/WO2_AC16.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/WO2_AC16.thy Fri Jun 17 16:12:49 2005 +0200
@@ -14,7 +14,7 @@
contains m distinct elements (in fact is equipollent to s)
*)
-theory WO2_AC16 = AC_Equiv + AC16_lemmas + Cardinal_aux:
+theory WO2_AC16 imports AC_Equiv AC16_lemmas Cardinal_aux begin
(**** A recursive definition used in the proof of WO2 ==> AC16 ****)
--- a/src/ZF/AC/WO6_WO1.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
Fortunately order types made this proof also very easy.
*)
-theory WO6_WO1 = Cardinal_aux:
+theory WO6_WO1 imports Cardinal_aux begin
constdefs
(* Auxiliary definitions used in proof *)
--- a/src/ZF/Arith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Arith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -13,7 +13,7 @@
header{*Arithmetic Operators and Their Definitions*}
-theory Arith = Univ:
+theory Arith imports Univ begin
text{*Proofs about elementary arithmetic: addition, multiplication, etc.*}
--- a/src/ZF/ArithSimp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ArithSimp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
theory ArithSimp
imports Arith
-files "~~/src/Provers/Arith/cancel_numerals.ML"
+uses "~~/src/Provers/Arith/cancel_numerals.ML"
"~~/src/Provers/Arith/combine_numerals.ML"
"arith_data.ML"
--- a/src/ZF/Bool.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Bool.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Booleans in Zermelo-Fraenkel Set Theory*}
-theory Bool = pair:
+theory Bool imports pair begin
syntax
"1" :: i ("1")
--- a/src/ZF/Cardinal.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Cardinal.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Cardinal Numbers Without the Axiom of Choice*}
-theory Cardinal = OrderType + Finite + Nat + Sum:
+theory Cardinal imports OrderType Finite Nat Sum begin
constdefs
--- a/src/ZF/CardinalArith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/CardinalArith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Cardinal Arithmetic Without the Axiom of Choice*}
-theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
+theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begin
constdefs
--- a/src/ZF/Cardinal_AC.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Cardinal_AC.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Cardinal Arithmetic Using AC*}
-theory Cardinal_AC = CardinalArith + Zorn:
+theory Cardinal_AC imports CardinalArith Zorn begin
subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
--- a/src/ZF/Coind/Dynamic.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Dynamic.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-theory Dynamic = Values:
+theory Dynamic imports Values begin
consts
EvalRel :: i
--- a/src/ZF/Coind/ECR.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/ECR.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-theory ECR = Static + Dynamic:
+theory ECR imports Static Dynamic begin
(* The extended correspondence relation *)
--- a/src/ZF/Coind/Language.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Language.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-theory Language = Main:
+theory Language imports Main begin
consts
Const :: i (* Abstract type of constants *)
--- a/src/ZF/Coind/Map.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Map.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
*)
-theory Map = Main:
+theory Map imports Main begin
constdefs
TMap :: "[i,i] => i"
--- a/src/ZF/Coind/Static.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Static.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-theory Static = Values + Types:
+theory Static imports Values Types begin
(*** Basic correspondence relation -- not completely specified, as it is a
parameter of the proof. A concrete version could be defined inductively.
--- a/src/ZF/Coind/Types.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Types.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-theory Types = Language:
+theory Types imports Language begin
consts
Ty :: i (* Datatype of types *)
--- a/src/ZF/Coind/Values.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Values.thy Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-theory Values = Language + Map:
+theory Values imports Language Map begin
(* Values, values environments and associated operators *)
--- a/src/ZF/Constructible/AC_in_L.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The Axiom of Choice Holds in L! *}
-theory AC_in_L = Formula:
+theory AC_in_L imports Formula begin
subsection{*Extending a Wellordering over a List -- Lexicographic Power*}
--- a/src/ZF/Constructible/DPow_absolute.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {*Absoluteness for the Definable Powerset Function*}
-theory DPow_absolute = Satisfies_absolute:
+theory DPow_absolute imports Satisfies_absolute begin
subsection{*Preliminary Internalizations*}
--- a/src/ZF/Constructible/Datatype_absolute.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Absoluteness Properties for Recursive Datatypes*}
-theory Datatype_absolute = Formula + WF_absolute:
+theory Datatype_absolute imports Formula WF_absolute begin
subsection{*The lfp of a continuous function can be expressed as a union*}
--- a/src/ZF/Constructible/Formula.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Formula.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* First-Order Formulas and the Definition of the Class L *}
-theory Formula = Main:
+theory Formula imports Main begin
subsection{*Internalized formulas of FOL*}
--- a/src/ZF/Constructible/Internalize.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Internalize.thy Fri Jun 17 16:12:49 2005 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-theory Internalize = L_axioms + Datatype_absolute:
+theory Internalize imports L_axioms Datatype_absolute begin
subsection{*Internalized Forms of Data Structuring Operators*}
--- a/src/ZF/Constructible/L_axioms.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The ZF Axioms (Except Separation) in L *}
-theory L_axioms = Formula + Relative + Reflection + MetaExists:
+theory L_axioms imports Formula Relative Reflection MetaExists begin
text {* The class L satisfies the premises of locale @{text M_trivial} *}
--- a/src/ZF/Constructible/MetaExists.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/MetaExists.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*The meta-existential quantifier*}
-theory MetaExists = Main:
+theory MetaExists imports Main begin
text{*Allows quantification over any term having sort @{text logic}. Used to
quantify over classes. Yields a proposition rather than a FOL formula.*}
--- a/src/ZF/Constructible/Normal.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Normal.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Closed Unbounded Classes and Normal Functions*}
-theory Normal = Main:
+theory Normal imports Main begin
text{*
One source is the book
--- a/src/ZF/Constructible/Rank.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Rank.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {*Absoluteness for Order Types, Rank Functions and Well-Founded
Relations*}
-theory Rank = WF_absolute:
+theory Rank imports WF_absolute begin
subsection {*Order Types: A Direct Construction by Replacement*}
--- a/src/ZF/Constructible/Rank_Separation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Rank_Separation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {*Separation for Facts About Order Types, Rank Functions and
Well-Founded Relations*}
-theory Rank_Separation = Rank + Rec_Separation:
+theory Rank_Separation imports Rank Rec_Separation begin
text{*This theory proves all instances needed for locales
--- a/src/ZF/Constructible/Rec_Separation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Separation for Facts About Recursion*}
-theory Rec_Separation = Separation + Internalize:
+theory Rec_Separation imports Separation Internalize begin
text{*This theory proves all instances needed for locales @{text
"M_trancl"} and @{text "M_datatypes"}*}
--- a/src/ZF/Constructible/Reflection.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Reflection.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* The Reflection Theorem*}
-theory Reflection = Normal:
+theory Reflection imports Normal begin
lemma all_iff_not_ex_not: "(\<forall>x. P(x)) <-> (~ (\<exists>x. ~ P(x)))";
by blast
--- a/src/ZF/Constructible/Relative.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Relative.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Relativization and Absoluteness*}
-theory Relative = Main:
+theory Relative imports Main begin
subsection{* Relativized versions of standard set-theoretic concepts *}
--- a/src/ZF/Constructible/Satisfies_absolute.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Absoluteness for the Satisfies Relation on Formulas*}
-theory Satisfies_absolute = Datatype_absolute + Rec_Separation:
+theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin
subsection {*More Internalization*}
--- a/src/ZF/Constructible/Separation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Separation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*Early Instances of Separation and Strong Replacement*}
-theory Separation = L_axioms + WF_absolute:
+theory Separation imports L_axioms WF_absolute begin
text{*This theory proves all instances needed for locale @{text "M_basic"}*}
--- a/src/ZF/Constructible/WF_absolute.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Absoluteness of Well-Founded Recursion*}
-theory WF_absolute = WFrec:
+theory WF_absolute imports WFrec begin
subsection{*Transitive closure without fixedpoints*}
--- a/src/ZF/Constructible/WFrec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/WFrec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header{*Relativized Well-Founded Recursion*}
-theory WFrec = Wellorderings:
+theory WFrec imports Wellorderings begin
subsection{*General Lemmas*}
--- a/src/ZF/Constructible/Wellorderings.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Relativized Wellorderings*}
-theory Wellorderings = Relative:
+theory Wellorderings imports Relative begin
text{*We define functions analogous to @{term ordermap} @{term ordertype}
but without using recursion. Instead, there is a direct appeal
--- a/src/ZF/Datatype.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Datatype.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,9 +7,9 @@
header{*Datatype and CoDatatype Definitions*}
-theory Datatype = Inductive + Univ + QUniv
- files
+theory Datatype imports Inductive Univ QUniv
+ uses
"Tools/datatype_package.ML"
- "Tools/numeral_syntax.ML": (*belongs to theory Bin*)
+ "Tools/numeral_syntax.ML" begin (*belongs to theory Bin*)
end
--- a/src/ZF/Epsilon.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Epsilon.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Epsilon Induction and Recursion*}
-theory Epsilon = Nat:
+theory Epsilon imports Nat begin
constdefs
eclose :: "i=>i"
--- a/src/ZF/Finite.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Finite.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Finite Powerset Operator and Finite Function Space*}
-theory Finite = Inductive + Epsilon + Nat:
+theory Finite imports Inductive Epsilon Nat begin
(*The natural numbers as a datatype*)
rep_datatype
--- a/src/ZF/Fixedpt.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Fixedpt.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
-theory Fixedpt = equalities:
+theory Fixedpt imports equalities begin
constdefs
--- a/src/ZF/IMP/Com.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/IMP/Com.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Arithmetic expressions, boolean expressions, commands *}
-theory Com = Main:
+theory Com imports Main begin
subsection {* Arithmetic expressions *}
--- a/src/ZF/IMP/Denotation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/IMP/Denotation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Denotational semantics of expressions and commands *}
-theory Denotation = Com:
+theory Denotation imports Com begin
subsection {* Definitions *}
--- a/src/ZF/IMP/Equiv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/IMP/Equiv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Equivalence *}
-theory Equiv = Denotation + Com:
+theory Equiv imports Denotation Com begin
lemma aexp_iff [rule_format]:
"[| a \<in> aexp; sigma: loc -> nat |]
--- a/src/ZF/Induct/Acc.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Acc.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* The accessible part of a relation *}
-theory Acc = Main:
+theory Acc imports Main begin
text {*
Inductive definition of @{text "acc(r)"}; see \cite{paulin-tlca}.
--- a/src/ZF/Induct/Binary_Trees.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Binary_Trees.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Binary trees *}
-theory Binary_Trees = Main:
+theory Binary_Trees imports Main begin
subsection {* Datatype definition *}
--- a/src/ZF/Induct/Brouwer.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Brouwer.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Infinite branching datatype definitions *}
-theory Brouwer = Main_ZFC:
+theory Brouwer imports Main_ZFC begin
subsection {* The Brouwer ordinals *}
--- a/src/ZF/Induct/Comb.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Comb.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Combinatory Logic example: the Church-Rosser Theorem *}
-theory Comb = Main:
+theory Comb imports Main begin
text {*
Curiously, combinators do not include free variables.
--- a/src/ZF/Induct/Datatypes.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Datatypes.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Sample datatype definitions *}
-theory Datatypes = Main:
+theory Datatypes imports Main begin
subsection {* A type with four constructors *}
--- a/src/ZF/Induct/FoldSet.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/FoldSet.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
least left-commutative.
*)
-theory FoldSet = Main:
+theory FoldSet imports Main begin
consts fold_set :: "[i, i, [i,i]=>i, i] => i"
--- a/src/ZF/Induct/ListN.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/ListN.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Lists of n elements *}
-theory ListN = Main:
+theory ListN imports Main begin
text {*
Inductive definition of lists of @{text n} elements; see
--- a/src/ZF/Induct/Mutil.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Mutil.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* The Mutilated Chess Board Problem, formalized inductively *}
-theory Mutil = Main:
+theory Mutil imports Main begin
text {*
Originator is Max Black, according to J A Robinson. Popularized as
--- a/src/ZF/Induct/Ntree.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Ntree.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Datatype definition n-ary branching trees *}
-theory Ntree = Main:
+theory Ntree imports Main begin
text {*
Demonstrates a simple use of function space in a datatype
--- a/src/ZF/Induct/Primrec.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Primrec.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Primitive Recursive Functions: the inductive definition *}
-theory Primrec = Main:
+theory Primrec imports Main begin
text {*
Proof adopted from \cite{szasz}.
--- a/src/ZF/Induct/PropLog.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/PropLog.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Meta-theory of propositional logic *}
-theory PropLog = Main:
+theory PropLog imports Main begin
text {*
Datatype definition of propositional logic formulae and inductive
--- a/src/ZF/Induct/Rmap.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Rmap.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* An operator to ``map'' a relation over a list *}
-theory Rmap = Main:
+theory Rmap imports Main begin
consts
rmap :: "i=>i"
--- a/src/ZF/Induct/Term.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Term.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Terms over an alphabet *}
-theory Term = Main:
+theory Term imports Main begin
text {*
Illustrates the list functor (essentially the same type as in @{text
--- a/src/ZF/Induct/Tree_Forest.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Trees and forests, a mutually recursive type definition *}
-theory Tree_Forest = Main:
+theory Tree_Forest imports Main begin
subsection {* Datatype definition *}
--- a/src/ZF/Inductive.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Inductive.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,14 +7,14 @@
header{*Inductive and Coinductive Definitions*}
-theory Inductive = Fixedpt + QPair
- files
+theory Inductive imports Fixedpt QPair
+ uses
"ind_syntax.ML"
"Tools/cartprod.ML"
"Tools/ind_cases.ML"
"Tools/inductive_package.ML"
"Tools/induct_tacs.ML"
- "Tools/primrec_package.ML":
+ "Tools/primrec_package.ML" begin
setup IndCases.setup
setup DatatypeTactics.setup
--- a/src/ZF/InfDatatype.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/InfDatatype.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Infinite-Branching Datatype Definitions*}
-theory InfDatatype = Datatype + Univ + Finite + Cardinal_AC:
+theory InfDatatype imports Datatype Univ Finite Cardinal_AC begin
lemmas fun_Limit_VfromE =
Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]
--- a/src/ZF/Integ/Bin.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Integ/Bin.thy Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
header{*Arithmetic on Binary Integers*}
-theory Bin = Int + Datatype:
+theory Bin imports Int Datatype begin
consts bin :: i
datatype
--- a/src/ZF/Integ/EquivClass.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Integ/EquivClass.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Equivalence Relations*}
-theory EquivClass = Trancl + Perm:
+theory EquivClass imports Trancl Perm begin
constdefs
--- a/src/ZF/Integ/Int.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Integ/Int.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
-theory Int = EquivClass + ArithSimp:
+theory Int imports EquivClass ArithSimp begin
constdefs
intrel :: i
--- a/src/ZF/Integ/IntArith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Integ/IntArith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,5 +1,5 @@
-theory IntArith = Bin
-files "int_arith.ML":
+theory IntArith imports Bin
+uses "int_arith.ML" begin
end
--- a/src/ZF/Integ/IntDiv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Integ/IntDiv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -31,7 +31,7 @@
header{*The Division Operators Div and Mod*}
-theory IntDiv = IntArith + OrderArith:
+theory IntDiv imports IntArith OrderArith begin
constdefs
quorem :: "[i,i] => o"
--- a/src/ZF/List.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/List.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Lists in Zermelo-Fraenkel Set Theory*}
-theory List = Datatype + ArithSimp:
+theory List imports Datatype ArithSimp begin
consts
list :: "i=>i"
--- a/src/ZF/Main.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Main.thy Fri Jun 17 16:12:49 2005 +0200
@@ -2,7 +2,7 @@
header{*Theory Main: Everything Except AC*}
-theory Main = List + IntDiv + CardinalArith:
+theory Main imports List IntDiv CardinalArith begin
(*The theory of "iterates" logically belongs to Nat, but can't go there because
primrec isn't available into after Datatype. The only theories defined
--- a/src/ZF/Main_ZFC.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Main_ZFC.thy Fri Jun 17 16:12:49 2005 +0200
@@ -1,3 +1,3 @@
-theory Main_ZFC = Main + InfDatatype:
+theory Main_ZFC imports Main InfDatatype begin
end
--- a/src/ZF/Nat.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Nat.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*The Natural numbers As a Least Fixed Point*}
-theory Nat = OrdQuant + Bool:
+theory Nat imports OrdQuant Bool begin
constdefs
nat :: i
--- a/src/ZF/OrdQuant.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/OrdQuant.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {*Special quantifiers*}
-theory OrdQuant = Ordinal:
+theory OrdQuant imports Ordinal begin
subsection {*Quantifiers and union operator for ordinals*}
--- a/src/ZF/Order.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Order.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header{*Partial and Total Orderings: Basic Definitions and Properties*}
-theory Order = WF + Perm:
+theory Order imports WF Perm begin
constdefs
--- a/src/ZF/OrderArith.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/OrderArith.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
-theory OrderArith = Order + Sum + Ordinal:
+theory OrderArith imports Order Sum Ordinal begin
constdefs
(*disjoint sum of two relations; underlies ordinal addition*)
--- a/src/ZF/OrderType.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/OrderType.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Order Types and Ordinal Arithmetic*}
-theory OrderType = OrderArith + OrdQuant + Nat:
+theory OrderType imports OrderArith OrdQuant Nat begin
text{*The order type of a well-ordering is the least ordinal isomorphic to it.
Ordinal arithmetic is traditionally defined in terms of order types, as it is
--- a/src/ZF/Ordinal.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Ordinal.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Transitive Sets and Ordinals*}
-theory Ordinal = WF + Bool + equalities:
+theory Ordinal imports WF Bool equalities begin
constdefs
--- a/src/ZF/Perm.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Perm.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Injections, Surjections, Bijections, Composition*}
-theory Perm = func:
+theory Perm imports func begin
constdefs
--- a/src/ZF/QPair.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/QPair.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
-theory QPair = Sum + func:
+theory QPair imports Sum func begin
text{*For non-well-founded data
structures in ZF. Does not precisely follow Quine's construction. Thanks
--- a/src/ZF/QUniv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/QUniv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*A Small Universe for Lazy Recursive Types*}
-theory QUniv = Univ + QPair:
+theory QUniv imports Univ QPair begin
(*Disjoint sums as a datatype*)
rep_datatype
--- a/src/ZF/Resid/Confluence.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Resid/Confluence.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Logic Image: ZF
*)
-theory Confluence = Reduction:
+theory Confluence imports Reduction begin
constdefs
confluence :: "i=>o"
--- a/src/ZF/Resid/Redex.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Resid/Redex.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Logic Image: ZF
*)
-theory Redex = Main:
+theory Redex imports Main begin
consts
redexes :: i
--- a/src/ZF/Resid/Reduction.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Resid/Reduction.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Logic Image: ZF
*)
-theory Reduction = Residuals:
+theory Reduction imports Residuals begin
(**** Lambda-terms ****)
--- a/src/ZF/Resid/Residuals.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Resid/Residuals.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
*)
-theory Residuals = Substitution:
+theory Residuals imports Substitution begin
consts
Sres :: "i"
--- a/src/ZF/Resid/Substitution.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Resid/Substitution.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
Logic Image: ZF
*)
-theory Substitution = Redex:
+theory Substitution imports Redex begin
consts
lift_aux :: "i=>i"
--- a/src/ZF/Sum.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Sum.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Disjoint Sums*}
-theory Sum = Bool + equalities:
+theory Sum imports Bool equalities begin
text{*And the "Part" primitive for simultaneous recursive type definitions*}
--- a/src/ZF/Trancl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Trancl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Relations: Their General Properties and Transitive Closure*}
-theory Trancl = Fixedpt + Perm:
+theory Trancl imports Fixedpt Perm begin
constdefs
refl :: "[i,i]=>o"
--- a/src/ZF/UNITY/AllocBase.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/AllocBase.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Common declarations for Chandy and Charpentier's Allocator*}
-theory AllocBase = Follows + MultisetSum + Guar:
+theory AllocBase imports Follows MultisetSum Guar begin
consts
tokbag :: i (* tokbags could be multisets...or any ordered type?*)
--- a/src/ZF/UNITY/AllocImpl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Charpentier and Chandy, section 7 (page 17).
*)
-theory AllocImpl = ClientImpl:
+theory AllocImpl imports ClientImpl begin
consts
--- a/src/ZF/UNITY/ClientImpl.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
*)
-theory ClientImpl = AllocBase + Guar:
+theory ClientImpl imports AllocBase Guar begin
consts
ask :: i (* input history: tokens requested *)
--- a/src/ZF/UNITY/Comp.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Comp.thy Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
header{*Composition*}
-theory Comp = Union + Increasing:
+theory Comp imports Union Increasing begin
constdefs
--- a/src/ZF/UNITY/Distributor.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Distributor.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Distributor specification
*)
-theory Distributor = AllocBase + Follows + Guar + GenPrefix:
+theory Distributor imports AllocBase Follows Guar GenPrefix begin
text{*Distributor specification (the number of outputs is Nclients)*}
--- a/src/ZF/UNITY/FP.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/FP.thy Fri Jun 17 16:12:49 2005 +0200
@@ -10,7 +10,7 @@
header{*Fixed Point of a Program*}
-theory FP = UNITY:
+theory FP imports UNITY begin
constdefs
FP_Orig :: "i=>i"
--- a/src/ZF/UNITY/Follows.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Follows.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*The "Follows" relation of Charpentier and Sivilotte*}
-theory Follows = SubstAx + Increasing:
+theory Follows imports SubstAx Increasing begin
constdefs
Follows :: "[i, i, i=>i, i=>i] => i"
--- a/src/ZF/UNITY/Guar.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Guar.thy Fri Jun 17 16:12:49 2005 +0200
@@ -22,7 +22,7 @@
header{*The Chandy-Sanders Guarantees Operator*}
-theory Guar = Comp:
+theory Guar imports Comp begin
(* To be moved to theory WFair???? *)
--- a/src/ZF/UNITY/Increasing.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Increasing.thy Fri Jun 17 16:12:49 2005 +0200
@@ -9,7 +9,7 @@
header{*Charpentier's "Increasing" Relation*}
-theory Increasing = Constrains + Monotonicity:
+theory Increasing imports Constrains Monotonicity begin
constdefs
--- a/src/ZF/UNITY/Merge.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Merge.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
Merge specification
*)
-theory Merge = AllocBase + Follows + Guar + GenPrefix:
+theory Merge imports AllocBase Follows Guar GenPrefix begin
(** Merge specification (the number of inputs is Nclients) ***)
(** Parameter A represents the type of items to Merge **)
--- a/src/ZF/UNITY/Monotonicity.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Monotonicity.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Monotonicity of an Operator WRT a Relation*}
-theory Monotonicity = GenPrefix + MultisetSum:
+theory Monotonicity imports GenPrefix MultisetSum begin
constdefs
--- a/src/ZF/UNITY/State.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/State.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*UNITY Program States*}
-theory State = Main:
+theory State imports Main begin
consts var :: i
datatype var = Var("i \<in> list(nat)")
--- a/src/ZF/UNITY/UNITY.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/UNITY.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {*The Basic UNITY Theory*}
-theory UNITY = State:
+theory UNITY imports State begin
text{*The basic UNITY theory (revised version, based upon the "co" operator)
From Misra, "A Logic for Concurrent Programming", 1994.
--- a/src/ZF/UNITY/Union.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Union.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
*)
-theory Union = SubstAx + FP:
+theory Union imports SubstAx FP begin
constdefs
--- a/src/ZF/Univ.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Univ.thy Fri Jun 17 16:12:49 2005 +0200
@@ -11,7 +11,7 @@
header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*}
-theory Univ = Epsilon + Cardinal:
+theory Univ imports Epsilon Cardinal begin
constdefs
Vfrom :: "[i,i]=>i"
--- a/src/ZF/WF.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/WF.thy Fri Jun 17 16:12:49 2005 +0200
@@ -17,7 +17,7 @@
header{*Well-Founded Recursion*}
-theory WF = Trancl:
+theory WF imports Trancl begin
constdefs
wf :: "i=>o"
--- a/src/ZF/ZF.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ZF.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*Zermelo-Fraenkel Set Theory*}
-theory ZF = FOL:
+theory ZF imports FOL begin
global
--- a/src/ZF/Zorn.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Zorn.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Zorn's Lemma*}
-theory Zorn = OrderArith + AC + Inductive:
+theory Zorn imports OrderArith AC Inductive begin
text{*Based upon the unpublished article ``Towards the Mechanization of the
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*}
--- a/src/ZF/equalities.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/equalities.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Basic Equalities and Inclusions*}
-theory equalities = pair:
+theory equalities imports pair begin
text{*These cover union, intersection, converse, domain, range, etc. Philippe
de Groote proved many of the inclusions.*}
--- a/src/ZF/ex/BinEx.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/BinEx.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
Examples of performing binary arithmetic by simplification
*)
-theory BinEx = Main:
+theory BinEx imports Main begin
(*All runtimes below are on a 300MHz Pentium*)
lemma "#13 $+ #19 = #32"
--- a/src/ZF/ex/CoUnit.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/CoUnit.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header {* Trivial codatatype definitions, one of which goes wrong! *}
-theory CoUnit = Main:
+theory CoUnit imports Main begin
text {*
See discussion in: L C Paulson. A Concrete Final Coalgebra Theorem
--- a/src/ZF/ex/Commutation.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Commutation.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
ported from Isabelle/HOL by Sidi Ould Ehmety
*)
-theory Commutation = Main:
+theory Commutation imports Main begin
constdefs
square :: "[i, i, i, i] => o"
--- a/src/ZF/ex/Group.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Group.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Groups *}
-theory Group = Main:
+theory Group imports Main begin
text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
Markus Wenzel.*}
--- a/src/ZF/ex/LList.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/LList.thy Fri Jun 17 16:12:49 2005 +0200
@@ -14,7 +14,7 @@
a typing rule for it, based on some notion of "productivity..."
*)
-theory LList = Main:
+theory LList imports Main begin
consts
llist :: "i=>i";
--- a/src/ZF/ex/Limit.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Limit.thy Fri Jun 17 16:12:49 2005 +0200
@@ -19,7 +19,7 @@
(Proofs converted to Isar and tidied up considerably by lcp)
*)
-theory Limit = Main:
+theory Limit imports Main begin
constdefs
--- a/src/ZF/ex/NatSum.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/NatSum.thy Fri Jun 17 16:12:49 2005 +0200
@@ -17,7 +17,7 @@
*)
-theory NatSum = Main:
+theory NatSum imports Main begin
consts sum :: "[i=>i, i] => i"
primrec
--- a/src/ZF/ex/Primes.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Primes.thy Fri Jun 17 16:12:49 2005 +0200
@@ -6,7 +6,7 @@
header{*The Divides Relation and Euclid's algorithm for the GCD*}
-theory Primes = Main:
+theory Primes imports Main begin
constdefs
divides :: "[i,i]=>o" (infixl "dvd" 50)
"m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
--- a/src/ZF/ex/Ramsey.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Ramsey.thy Fri Jun 17 16:12:49 2005 +0200
@@ -26,7 +26,7 @@
*)
-theory Ramsey = Main:
+theory Ramsey imports Main begin
constdefs
Symmetric :: "i=>o"
"Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)"
--- a/src/ZF/ex/Ring.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/Ring.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Rings *}
-theory Ring = Group:
+theory Ring imports Group begin
(*First, we must simulate a record declaration:
record ring = monoid +
--- a/src/ZF/ex/misc.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/ex/misc.thy Fri Jun 17 16:12:49 2005 +0200
@@ -8,7 +8,7 @@
header{*Miscellaneous ZF Examples*}
-theory misc = Main:
+theory misc imports Main begin
subsection{*Various Small Problems*}
--- a/src/ZF/func.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/func.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
header{*Functions, Function Spaces, Lambda-Abstraction*}
-theory func = equalities + Sum:
+theory func imports equalities Sum begin
subsection{*The Pi Operator: Dependent Function Space*}
--- a/src/ZF/pair.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/pair.thy Fri Jun 17 16:12:49 2005 +0200
@@ -7,8 +7,8 @@
header{*Ordered Pairs*}
-theory pair = upair
-files "simpdata.ML":
+theory pair imports upair
+uses "simpdata.ML" begin
(** Lemmas for showing that <a,b> uniquely determines a and b **)
--- a/src/ZF/upair.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/upair.thy Fri Jun 17 16:12:49 2005 +0200
@@ -12,8 +12,8 @@
header{*Unordered Pairs*}
-theory upair = ZF
-files "Tools/typechk.ML":
+theory upair imports ZF
+uses "Tools/typechk.ML" begin
setup TypeCheck.setup