# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1249310821 -7200
# Node ID 0cbd34857b9e6f49d9dfd2c1485b24a5cc6474a3
# Parent  2728e8daebc05e50d58ee9600fd7c3337a7bc7a9
tuned

diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/Base.thy	Mon Aug 03 16:47:01 2009 +0200
@@ -6,6 +6,7 @@
   "antiquote_setup.ML"
 begin
 
+(* re-definition of various ML antiquotations    *)
 (* to have a special tag for text enclosed in ML *)
 
 ML {*
diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/Intro.thy	Mon Aug 03 16:47:01 2009 +0200
@@ -175,7 +175,7 @@
   times.) The most important conventions are:
 
   \begin{itemize}
-  \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term}
+  \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
   \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
   \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
   \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Aug 03 16:47:01 2009 +0200
@@ -1060,7 +1060,6 @@
   \begin{readmore}
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
-  The function @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in @{ML_file "Pure/subgoal.ML"}
   \end{readmore}
 
 *}
diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Mon Aug 03 16:47:01 2009 +0200
@@ -47,8 +47,8 @@
   (eval_fn ctxt (ml_val_open ovars istruc txt);
    case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt)  of
      (NONE, bn, "")  => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
-   | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruc qn}
-   | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruc st})
+   | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn}
+   | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st})
 
 val parser_ml = Scan.lift (Args.name --
   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
diff -r 2728e8daebc0 -r 0cbd34857b9e ProgTutorial/output_tutorial.ML
--- a/ProgTutorial/output_tutorial.ML	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Mon Aug 03 16:47:01 2009 +0200
@@ -3,7 +3,7 @@
 struct
 
 (* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos, index]                   *)
+(* enable the options [gray, linenos, index]                 *)
 
 val gray = ref false
 val linenos = ref false
@@ -26,11 +26,12 @@
     #> enclose "\\isa{" "}")
 end
 
+
 datatype qstring =
   NoString
-| Plain  of string
-| Code   of string
-| IStruc of string
+| Plain   of string
+| Code    of string
+| IStruct of string
 
 datatype entry = 
    No_Entry
@@ -67,7 +68,7 @@
 fun get_qstring NoString = ""
   | get_qstring (Plain s) = get_word s
   | get_qstring (Code s) = let val w = get_word s in  (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end
-  | get_qstring (IStruc s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
+  | get_qstring (IStruct s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
 
 fun is_empty_qstr (Plain "") = true
   | is_empty_qstr (Code "") = true
diff -r 2728e8daebc0 -r 0cbd34857b9e progtutorial.pdf
Binary file progtutorial.pdf has changed