# HG changeset patch # User nipkow # Date 1363254688 -3600 # Node ID 0098bfe3be53f59abe5fe8b2059d125b43f6839c # Parent d2dfd743b58cddfdbbc1dde6aa313a9bb2591ab9 tuned diff -r d2dfd743b58c -r 0098bfe3be53 src/Doc/ProgProve/Logic.thy --- a/src/Doc/ProgProve/Logic.thy Wed Mar 13 22:46:28 2013 +0100 +++ b/src/Doc/ProgProve/Logic.thy Thu Mar 14 10:51:28 2013 +0100 @@ -81,10 +81,10 @@ \item @{prop"e \ A"},\quad @{prop"A \ B"} \item @{term"A \ B"},\quad @{term"A \ B"},\quad @{term"A - B"},\quad @{term"-A"} \end{itemize} +(where @{term"A-B"} and @{text"-A"} are set difference and complement) and much more. @{const UNIV} is the set of all elements of some type. Set comprehension is written @{term"{x. P}"} -rather than @{text"{x | P}"}, to emphasize the variable binding nature -of the construct. +rather than @{text"{x | P}"}. \begin{warn} In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension involving a proper term @{text t} must be written diff -r d2dfd743b58c -r 0098bfe3be53 src/HOL/IMP/Live.thy --- a/src/HOL/IMP/Live.thy Wed Mar 13 22:46:28 2013 +0100 +++ b/src/HOL/IMP/Live.thy Thu Mar 14 10:51:28 2013 +0100 @@ -7,14 +7,12 @@ subsection "Liveness Analysis" -text_raw{*\snip{LDef}{0}{2}{% *} fun L :: "com \ vname set \ vname set" where -"L SKIP X = X" | +"L SKIP X = X" | "L (x ::= a) X = (X - {x}) \ vars a" | -"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \ L c\<^isub>2) X" | +"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" | "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \ L c\<^isub>1 X \ L c\<^isub>2 X" | -"L (WHILE b DO c) X = vars b \ X \ L c X" -text_raw{*}%endsnip*} +"L (WHILE b DO c) X = vars b \ X \ L c X" value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"