# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265381343 -3600
# Node ID c6b5d1e25cdd39376512382cd5c5ba5cf436406c
# Parent  dc76ba24e81bbeaf1f953c225008a6126182e9c2
updated to new Isabelle

diff -r dc76ba24e81b -r c6b5d1e25cdd ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Thu Jan 14 22:10:04 2010 +0100
+++ b/ProgTutorial/Essential.thy	Fri Feb 05 15:49:03 2010 +0100
@@ -39,7 +39,7 @@
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
 "Const (\"op =\", \<dots>) $ 
-  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+  (Const (\"Algebras.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
@@ -533,8 +533,8 @@
   \mbox{@{text "(op *)"}}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
- "(Const (\"HOL.zero_class.zero\", \<dots>), 
- Const (\"HOL.times_class.times\", \<dots>))"}
+ "(Const (\"Algebras.zero_class.zero\", \<dots>), 
+ Const (\"Algebras.times_class.times\", \<dots>))"}
 
   While you could use the complete name, for example 
   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
diff -r dc76ba24e81b -r c6b5d1e25cdd ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Jan 14 22:10:04 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Feb 05 15:49:03 2010 +0100
@@ -2178,7 +2178,7 @@
 end"
 "Const (\"==\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
-    (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
+    (Const (\"Algebras.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
   the right-hand side should be fully beta-normalised. If instead 
diff -r dc76ba24e81b -r c6b5d1e25cdd progtutorial.pdf
Binary file progtutorial.pdf has changed