# HG changeset patch
# User wenzelm
# Date 1129751527 -7200
# Node ID 99ead7a7eb42bf044fe6e22f5bbe4f778512d4f9
# Parent  4159e1523ad82878ec5c8be07d705cd9e27e91f9
fix headers;

diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/IsarOverview/Isar/Induction.thy
--- a/doc-src/IsarOverview/Isar/Induction.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Induction = Main:(*>*)
+(*<*)theory Induction imports Main begin(*>*)
 
 section{*Case distinction and induction \label{sec:Induct}*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/IsarOverview/Isar/Logic.thy
--- a/doc-src/IsarOverview/Isar/Logic.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Logic = Main:(*>*)
+(*<*)theory Logic imports Main begin(*>*)
 
 section{*Logic \label{sec:Logic}*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Partial = While_Combinator:(*>*)
+(*<*)theory Partial imports While_Combinator begin(*>*)
 
 text{*\noindent Throughout this tutorial, we have emphasized
 that all functions in HOL are total.  We cannot hope to define
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory WFrec = Main:(*>*)
+(*<*)theory WFrec imports Main begin(*>*)
 
 text{*\noindent
 So far, all recursive definitions were shown to terminate via measure
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/CTL/Base.thy
--- a/doc-src/TutorialI/CTL/Base.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Base = Main:(*>*)
+(*<*)theory Base imports Main begin(*>*)
 
 section{*Case Study: Verified Model Checking*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory CTL = Base:;(*>*)
+(*<*)theory CTL imports Base begin(*>*)
 
 subsection{*Computation Tree Logic --- CTL*};
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/CTL/CTLind.thy
--- a/doc-src/TutorialI/CTL/CTLind.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory CTLind = CTL:(*>*)
+(*<*)theory CTLind imports CTL begin(*>*)
 
 subsection{*CTL Revisited*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory PDL = Base:(*>*)
+(*<*)theory PDL imports Base begin(*>*)
 
 subsection{*Propositional Dynamic Logic --- PDL*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory AB = Main:(*>*)
+(*<*)theory AB imports Main begin(*>*)
 
 section{*Case Study: A Context Free Grammar*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Inductive/Mutual.thy
--- a/doc-src/TutorialI/Inductive/Mutual.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Inductive/Mutual.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Mutual = Main:(*>*)
+(*<*)theory Mutual imports Main begin(*>*)
 
 subsection{*Mutually Inductive Definitions*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Inductive/Star.thy
--- a/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Star = Main:(*>*)
+(*<*)theory Star imports Main begin(*>*)
 
 section{*The Reflexive Transitive Closure*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Misc/types.thy
--- a/doc-src/TutorialI/Misc/types.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Misc/types.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory "types" = Main:(*>*)
+(*<*)theory "types" imports Main begin(*>*)
 types number       = nat
       gate         = "bool \<Rightarrow> bool \<Rightarrow> bool"
       ('a,'b)alist = "('a \<times> 'b)list"
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Axioms.thy
--- a/doc-src/TutorialI/Types/Axioms.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Axioms = Overloading:(*>*)
+(*<*)theory Axioms imports Overloading begin(*>*)
 
 subsection{*Axioms*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Overloading.thy
--- a/doc-src/TutorialI/Types/Overloading.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Overloading = Overloading1:(*>*)
+(*<*)theory Overloading imports Overloading1 begin(*>*)
 instance list :: (type)ordrel
 by intro_classes
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Overloading0.thy
--- a/doc-src/TutorialI/Types/Overloading0.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Overloading0.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Overloading0 = Main:(*>*)
+(*<*)theory Overloading0 imports Main begin(*>*)
 
 text{* We start with a concept that is required for type classes but already
 useful on its own: \emph{overloading}. Isabelle allows overloading: a
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Overloading1.thy
--- a/doc-src/TutorialI/Types/Overloading1.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Overloading1 = Main:(*>*)
+(*<*)theory Overloading1 imports Main begin(*>*)
 
 subsubsection{*Controlled Overloading with Type Classes*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Overloading2.thy
--- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Overloading2 = Overloading1:(*>*)
+(*<*)theory Overloading2 imports Overloading1 begin(*>*)
 
 text{*
 Of course this is not the only possible definition of the two relations.
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Pairs.thy
--- a/doc-src/TutorialI/Types/Pairs.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Pairs.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Pairs = Main:(*>*)
+(*<*)theory Pairs imports Main begin(*>*)
 
 section{*Pairs and Tuples*}
 
diff -r 4159e1523ad8 -r 99ead7a7eb42 doc-src/TutorialI/Types/Typedefs.thy
--- a/doc-src/TutorialI/Types/Typedefs.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Typedefs = Main:(*>*)
+(*<*)theory Typedefs imports Main begin(*>*)
 
 section{*Introducing New Types*}