# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1248624830 -7200
# Node ID 6af069ab43d49341c5c943c2a6c6ff42ec8a0538
# Parent  08ffafe2585d154619387bbd8b371c3bf6639261
slight change

diff -r 08ffafe2585d -r 6af069ab43d4 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sun Jul 26 13:06:55 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Jul 26 18:13:50 2009 +0200
@@ -993,7 +993,7 @@
   type-classes. Consider for example the constants for @{term "zero"} and
   \mbox{@{text "(op *)"}}:
 
-  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
+  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
  "(Const (\"HOL.zero_class.zero\", \<dots>), 
  Const (\"HOL.times_class.times\", \<dots>))"}
 
diff -r 08ffafe2585d -r 6af069ab43d4 progtutorial.pdf
Binary file progtutorial.pdf has changed