# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282973845 -28800
# Node ID 102dc5cc1aed2616dca5a9c4f9c518fb99309243
# Parent  f952f2679a113407077fab32f84eae0f9255f32e
a bit closer to the new conventions of naming HOL-constants

diff -r f952f2679a11 -r 102dc5cc1aed ProgTutorial/First_Steps.thy
--- 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
diff -r f952f2679a11 -r 102dc5cc1aed progtutorial.pdf
Binary file progtutorial.pdf has changed