# HG changeset patch # User griff # Date 1248175659 -7200 # Node ID 4b97bff55650cda1af0c2a2c4db123f3fa92d780 # Parent f9f3ecc949c5f151165d52045cbcd29a14c7f741 show type of "x" diff -r f9f3ecc949c5 -r 4b97bff55650 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Tue Jul 21 13:22:17 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Tue Jul 21 13:27:39 2009 +0200 @@ -935,7 +935,7 @@ | is_all _ = false*} text {* - will not correctly match the formula @{prop "\x::nat. P x"}: + will not correctly match the formula @{prop[source] "\x::nat. P x"}: @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "false"} diff -r f9f3ecc949c5 -r 4b97bff55650 progtutorial.pdf Binary file progtutorial.pdf has changed