--- a/ProgTutorial/General.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/General.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -11,7 +11,7 @@
 (*>*)
 
 
-chapter {* Isabelle in More Detail *}
+chapter {* Isabelle Essentials *}
 
 text {*
   Isabelle is build around a few central ideas. One central idea is the
@@ -886,14 +886,13 @@
 
   Recall that Isabelle does not let you call @{ML note in LocalTheory} twice
   with the same theorem name. In effect, once a theorem is stored under a name, 
-  this association will be fixed. While this is a ``safety-net'' to make sure a
+  this association is fixed. While this is a ``safety-net'' to make sure a
   theorem name refers to a particular theorem or collection of theorems, it is 
   also a bit too restrictive in cases where a theorem name should refer to a 
   dynamically expanding list of theorems (like a simpset). Therefore Isabelle 
   also implements a mechanism where a theorem name can refer to a custom theorem 
   list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. 
-  To see how it works let us assume we defined our own theorem list maintained 
-  in the data storage @{text MyThmList}.
+  To see how it works let us assume we defined our own theorem list @{text MyThmList}.
 *}
 
 ML{*structure MyThmList = GenericDataFun
@@ -945,8 +944,8 @@
   @{text "> True"}
   \end{isabelle}
 
-  There is a multitude of functions that manage or manipulate theorems in the 
-  structures @{ML_struct Thm} and @{ML_struct Drule}. For example 
+  There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule} 
+  for managing or manipulating theorems. For example 
   we can test theorems for alpha equality. Suppose you proved the following three 
   theorems.
 *}
@@ -1008,8 +1007,7 @@
   Note that in the second case, there is no premise.
 
   \begin{readmore}
-  For the functions @{text "assume"}, @{text "forall_elim"} etc 
-  see \isccite{sec:thms}. The basic functions for theorems are defined in
+  The basic functions for theorems are defined in
   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
@@ -1191,10 +1189,10 @@
   term stands for the theorem to be presented; the output can be constructed to
   ones wishes.  Let us, for example, assume we want to quote theorems without
   leading @{text \<forall>}-quantifiers. For this we can implement the following function 
-  that strips off meta-quantifiers.
+  that strips off @{text "\<forall>"}s.
 *}
 
-ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
+ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
       Term.dest_abs body |> snd |> strip_allq
   | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = 
       strip_allq t
@@ -1243,7 +1241,7 @@
   and uses them as name in the outermost abstractions.
 *}
 
-ML {*fun rename_allq [] t = t
+ML{*fun rename_allq [] t = t
   | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
       Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
   | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
@@ -1506,6 +1504,49 @@
   \end{readmore}
 *}
 
+section {* Theories\label{sec:theories} (TBD) *}
+
+
+text {*
+  Theories are the most fundamental building blocks in Isabelle. They 
+  contain definitions, syntax declarations, axioms, proofs etc. If a definition
+  is stated, it must be stored in a theory in order to be usable later
+  on. Similar with proofs: once a proof is finished, the proved theorem
+  needs to be stored in the theorem database of the theory in order to
+  be usable. All relevant data of a theort can be querried as follows.
+
+  \begin{isabelle}
+  \isacommand{print\_theory}\\
+  @{text "> names: Pure Code_Generator HOL \<dots>"}\\
+  @{text "> classes: Inf < type \<dots>"}\\
+  @{text "> default sort: type"}\\
+  @{text "> syntactic types: #prop \<dots>"}\\
+  @{text "> logical types: 'a \<times> 'b \<dots>"}\\
+  @{text "> type arities: * :: (random, random) random \<dots>"}\\
+  @{text "> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>"}\\
+  @{text "> abbreviations: \<dots>"}\\
+  @{text "> axioms: \<dots>"}\\
+  @{text "> oracles: \<dots>"}\\
+  @{text "> definitions: \<dots>"}\\
+  @{text "> theorems: \<dots>"}
+  \end{isabelle}
+
+  \begin{center}
+  \begin{tikzpicture}
+  \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A};
+  \end{tikzpicture}
+  \end{center}
+
+
+  In contrast to an ordinary theory, which simply consists of a type
+  signature, as well as tables for constants, axioms and theorems, a local
+  theory contains additional context information, such as locally fixed
+  variables and local assumptions that may be used by the package. The type
+  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
+  @{ML_type "Proof.context"}, although not every proof context constitutes a
+  valid local theory.
+*}
+
 section {* Setups (TBD) *}
 
 text {*
@@ -1559,21 +1600,6 @@
   the current simpset.
 *}
 
-section {* Theories\label{sec:theories} (TBD) *}
-
-text {*
-  There are theories, proof contexts and local theories (in this order, if you
-  want to order them). 
-
-  In contrast to an ordinary theory, which simply consists of a type
-  signature, as well as tables for constants, axioms and theorems, a local
-  theory contains additional context information, such as locally fixed
-  variables and local assumptions that may be used by the package. The type
-  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
-  @{ML_type "Proof.context"}, although not every proof context constitutes a
-  valid local theory.
-*}
-
 section {* Contexts (TBD) *}
 
 section {* Local Theories (TBD) *}