--- a/ProgTutorial/First_Steps.thy	Sat Aug 28 13:27:16 2010 +0800
+++ b/ProgTutorial/First_Steps.thy	Sat Aug 28 13:37:25 2010 +0800
@@ -1100,9 +1100,9 @@
 *}
 
 setup %gray {*
-  update "op &"   @{thm conjI} #>
-  update "op -->" @{thm impI}  #>
-  update "All"    @{thm allI}
+  update "conj" @{thm conjI} #>
+  update "imp"  @{thm impI}  #>
+  update "all"  @{thm allI}
 *}
 
 text {*
@@ -1111,7 +1111,7 @@
   section~\ref{sec:theories}). The lookup can now be performed as follows.
 
   @{ML_response_fake [display, gray]
-"lookup @{theory} \"op &\""
+"lookup @{theory} \"conj\""
 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
 
   An important point to note is that these tables (and data in general)
@@ -1119,13 +1119,13 @@
   we can update the table as follows
 *}
 
-setup %gray {* update "op &" @{thm TrueI} *}
+setup %gray {* update "conj" @{thm TrueI} *}
 
 text {*
   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
   
 @{ML_response_fake [display, gray]
-"lookup @{theory} \"op &\""
+"lookup @{theory} \"conj\""
 "SOME \"True\""}
 
   there are no references involved. This is one of the most fundamental