# HG changeset patch
# User nipkow
# Date 1363114517 -3600
# Node ID f4c82c165f589fa309c17b105837150ed15dc9e0
# Parent  bbb7639554dc18f9ef9ea3d4d32c44996bd4df96
added latex markup

diff -r bbb7639554dc -r f4c82c165f58 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Tue Mar 12 11:59:26 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Tue Mar 12 19:55:17 2013 +0100
@@ -7,12 +7,14 @@
 
 subsection "Liveness Analysis"
 
+text_raw{*\snip{LDef}{0}{2}{% *}
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
-"L SKIP X = X" |
-"L (x ::= a) X = X-{x} \<union> vars a" |
-"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
+"L SKIP     X = X" |
+"L (x ::= a) X = (X - {x}) \<union> vars a" |
+"L (c\<^isub>1; c\<^isub>2)  X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
-"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
+"L (WHILE b DO c)          X = vars b \<union> X \<union> L c X"
+text_raw{*}%endsnip*}
 
 value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"