Mercurial Mercurial > hg > isabelle-cookbook / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Essential.thy
changeset 554 638ed040e6f8
parent 553 c53d74b34123
child 555 2c34c69236ce 
--- a/ProgTutorial/Essential.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/Essential.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -192,8 +192,8 @@
   where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
-  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, 
- Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
+  "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>, 
+ Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"}
 
   where it is not (since it is already constructed by a meta-implication). 
   The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
isabelle-cookbook