# HG changeset patch
# User haftmann
# Date 1275319768 -7200
# Node ID 32a6f471f090a305721f51dc057ddedb2cf29b9a
# Parent  1f1f9cbd23ae39520cbf9079a3edc0416c1510d4
clarified

diff -r 1f1f9cbd23ae -r 32a6f471f090 doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Mon May 31 17:29:26 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy	Mon May 31 17:29:28 2010 +0200
@@ -172,22 +172,22 @@
      \item replacing non-executable constructs by executable ones:
 *}     
 
-lemma %quote [code_inline]:
-  "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+lemma %quote [code_unfold]:
+  "x \<in> set xs \<longleftrightarrow> member xs x" by (fact in_set_code)
 
 text {*
      \item eliminating superfluous constants:
 *}
 
-lemma %quote [code_inline]:
-  "1 = Suc 0" by simp
+lemma %quote [code_unfold]:
+  "1 = Suc 0" by (fact One_nat_def)
 
 text {*
      \item replacing executable but inconvenient constructs:
 *}
 
-lemma %quote [code_inline]:
-  "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
+lemma %quote [code_unfold]:
+  "xs = [] \<longleftrightarrow> List.null xs" by (fact empty_null)
 
 text_raw {*
   \end{itemize}