--- a/ProgTutorial/Tactical.thy	Mon Aug 03 16:47:01 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Tue Aug 04 16:18:39 2009 +0200
@@ -17,6 +17,7 @@
 
 *}
 
+
 section {* Basics of Reasoning with Tactics*}
 
 text {*
@@ -222,6 +223,8 @@
   \begin{boxedminipage}{\textwidth}
   \begin{isabelle}
 *}
+notation (output) "prop"  ("#_" [1000] 1000)
+
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
 apply(tactic {* my_print_tac @{context} *})
 
@@ -233,7 +236,7 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
 *}
@@ -249,7 +252,7 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
 *}
@@ -265,7 +268,7 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
 *}
@@ -281,11 +284,11 @@
       \small\colorbox{gray!20}{
       \begin{tabular}{@ {}l@ {}}
       internal goal state:\\
-      @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+      @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip   
    *}
-done
+(*<*)oops(*>*)
 text_raw {*  
   \end{isabelle}
   \end{boxedminipage}
@@ -294,8 +297,8 @@
   the goal state as represented internally (highlighted boxes). This
   tactic shows that every goal state in Isabelle is represented by a theorem:
   when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
-  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
-  theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
+  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
+  theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}.\label{fig:goalstates}}
   \end{figure}
 *}
 
@@ -307,17 +310,17 @@
   proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, 
   internally every goal state is an implication of the form
 
-  @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
+  @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
 
   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
   the subgoals. So after setting up the lemma, the goal state is always of the
-  form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
-  "(C)"}.\footnote{This only applies to single statements. If the lemma
+  form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
+  "#C"}.\footnote{This only applies to single statements. If the lemma
   contains more than one statement, then one has more such implications.} 
   Since the goal @{term C} can potentially be an implication, there is a
   ``protector'' wrapped around it (the wrapper is the outermost constant
-  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible
-  in the figure). This wrapper prevents that premises of @{text C} are
+  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
+  as an @{text #}). This wrapper prevents that premises of @{text C} are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic