# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1320662965 0
# Node ID 1c4250bc6258286d506729646065c378c696c61d
# Parent  45cfd2ece7bd8aeaaacbdc24e6226463eb9980b2
more on theories

diff -r 45cfd2ece7bd -r 1c4250bc6258 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Sun Nov 06 15:15:59 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Mon Nov 07 10:49:25 2011 +0000
@@ -23,8 +23,8 @@
   While terms, types and theorems are the most basic data structures in
   Isabelle, there are a number of layers built on top of them. Most of these
   layers are concerned with storing and manipulating data. Handling them
-  properly is an essential skill for programming on the ML-level of Isabelle
-  programming. The most basic layer are theories. They contain global data and
+  properly is an essential skill for programming on the ML-level of Isabelle. 
+  The most basic layer are theories. They contain global data and
   can be seen as the ``long-term memory'' of Isabelle. There is usually only
   one theory active at each moment. Proof contexts and local theories, on the
   other hand, store local data for a task at hand. They act like the
@@ -35,12 +35,12 @@
 section {* Theories and Setups\label{sec:theories} *}
 
 text {*
-  Theories, as said above, are the most basic layer of abstraction in
-  Isabelle. They contain definitions, syntax declarations, axioms, proofs
-  and much more. If a definition is made, 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 theory can be queried as follows.
+  Theories, as said above, are a basic layer of abstraction in Isabelle. They
+  contain definitions, syntax declarations, axioms, theorems and much more. If a
+  definition is made, 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 theory can be queried as follows.
 
   \begin{isabelle}
   \isacommand{print\_theory}\\
@@ -58,6 +58,15 @@
   @{text "> theorems: \<dots>"}
   \end{isabelle}
 
+  Functions acting on theories often end with the suffix @{text "_global"},
+  for example the function @{ML read_term_global in Syntax} in the structure
+  @{ML_struct Syntax}. The reason is to set them syntactically apart from
+  functions acting on contexts or local theories (which will be discussed in
+  next sections). There is a tendency in the Isabelle development to prefer
+  ``non-global'' operations, because they have some advantages, as we will also
+  discuss later. However, some basic management of theories will very likely
+  never go away.
+
   In the context ML-programming, the most important command with theories
   is \isacommand{setup}. In the previous chapters we used it, for
   example, to make a theorem attribute known to Isabelle or to register a theorem
@@ -196,6 +205,7 @@
 ML{*Proof_Context.verbose := true*}
 *)
 
+(*
 lemma "True"
 proof -
   { -- "\<And>x. _"
@@ -222,7 +232,7 @@
   thm this
 
 oops
-
+*)
 
 section {* Local Theories (TBD) *}
 
diff -r 45cfd2ece7bd -r 1c4250bc6258 progtutorial.pdf
Binary file progtutorial.pdf has changed