1.1 --- a/doc-src/Codegen/Thy/Program.thy	Mon May 31 17:29:26 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Program.thy	Mon May 31 17:29:28 2010 +0200
     1.3 @@ -172,22 +172,22 @@
     1.4       \item replacing non-executable constructs by executable ones:
     1.5  *}     
     1.6  
     1.7 -lemma %quote [code_inline]:
     1.8 -  "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
     1.9 +lemma %quote [code_unfold]:
    1.10 +  "x \<in> set xs \<longleftrightarrow> member xs x" by (fact in_set_code)
    1.11  
    1.12  text {*
    1.13       \item eliminating superfluous constants:
    1.14  *}
    1.15  
    1.16 -lemma %quote [code_inline]:
    1.17 -  "1 = Suc 0" by simp
    1.18 +lemma %quote [code_unfold]:
    1.19 +  "1 = Suc 0" by (fact One_nat_def)
    1.20  
    1.21  text {*
    1.22       \item replacing executable but inconvenient constructs:
    1.23  *}
    1.24  
    1.25 -lemma %quote [code_inline]:
    1.26 -  "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
    1.27 +lemma %quote [code_unfold]:
    1.28 +  "xs = [] \<longleftrightarrow> List.null xs" by (fact empty_null)
    1.29  
    1.30  text_raw {*
    1.31    \end{itemize}