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.
show the type of "x" in the formula
authorgriff
Tue, 21 Jul 2009 12:05:15 +0200
changeset 269 3e084d62885c
parent 268 509e2ca547db
child 270 bfcabed9079e
show the type of "x" in the formula
ProgTutorial/FirstSteps.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- a/ProgTutorial/FirstSteps.thy	Tue Jul 21 11:59:09 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 21 12:05:15 2009 +0200
@@ -803,7 +803,7 @@
   | is_all _ = false*}
 
 text {* 
-  will not correctly match the formula @{prop "\<forall>x::nat. P x"}: 
+  will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 
 
   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
Binary file progtutorial.pdf has changed
isabelle-cookbook