Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
slight change
authorChristian Urban <urbanc@in.tum.de>
Sun, 26 Jul 2009 18:13:50 +0200
changeset 290 6af069ab43d4
parent 289 08ffafe2585d
child 291 077c764c8d8b
slight change
ProgTutorial/FirstSteps.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- 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>))"}
 
Binary file progtutorial.pdf has changed
isabelle-cookbook