# HG changeset patch
# User wenzelm
# Date 1326296850 -3600
# Node ID f009e0fe86438dab613c7ecebb0de7db208c770c
# Parent  9ae331a1d8c55297ff7bd0c5cdb6c5002c5622a6
updated example -- List.foldl is no longer defined via primrec;

diff -r 9ae331a1d8c5 -r f009e0fe8643 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jan 11 16:25:34 2012 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jan 11 16:47:30 2012 +0100
@@ -267,8 +267,8 @@
 
 The advantage of the display option is that you can display a whole
 list of theorems in one go. For example,
-\verb!@!\verb!{thm[display] foldl.simps}!
-generates @{thm[display] foldl.simps}
+\verb!@!\verb!{thm[display] append.simps}!
+generates @{thm[display] append.simps}
 *}
 
 subsection "If-then"
@@ -413,16 +413,16 @@
   the output
   \begin{center}
   \begin{tabular}{l@ {~~@{text "="}~~}l}
-  @{thm (lhs) foldl_Nil} & @{thm (rhs) foldl_Nil}\\
-  @{thm (lhs) foldl_Cons} & @{thm (rhs) foldl_Cons}
+  @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
+  @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
   \end{tabular}
   \end{center}
   is produced by the following code:
   \begin{quote}
     \verb!\begin{center}!\\
     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
-    \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
-    \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
+    \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
+    \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
     \verb!\end{tabular}!\\
     \verb!\end{center}!
   \end{quote}
diff -r 9ae331a1d8c5 -r f009e0fe8643 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jan 11 16:25:34 2012 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Jan 11 16:47:30 2012 +0100
@@ -337,10 +337,10 @@
 
 The advantage of the display option is that you can display a whole
 list of theorems in one go. For example,
-\verb!@!\verb!{thm[display] foldl.simps}!
+\verb!@!\verb!{thm[display] append.simps}!
 generates \begin{isabelle}%
-foldl\ f\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ a\isasep\isanewline%
-foldl\ f\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ foldl\ f\ {\isaliteral{28}{\isacharparenleft}}f\ a\ x{\isaliteral{29}{\isacharparenright}}\ xs%
+{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isacharat\ ys\ {\isaliteral{3D}{\isacharequal}}\ ys\isasep\isanewline%
+x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys%
 \end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -522,16 +522,16 @@
   the output
   \begin{center}
   \begin{tabular}{l@ {~~\isa{{\isaliteral{3D}{\isacharequal}}}~~}l}
-  \isa{foldl\ f\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} & \isa{a}\\
-  \isa{foldl\ f\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs{\isaliteral{29}{\isacharparenright}}} & \isa{foldl\ f\ {\isaliteral{28}{\isacharparenleft}}f\ a\ x{\isaliteral{29}{\isacharparenright}}\ xs}
+  \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isacharat\ ys} & \isa{ys}\\
+  \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys} & \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys}
   \end{tabular}
   \end{center}
   is produced by the following code:
   \begin{quote}
     \verb!\begin{center}!\\
     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
-    \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
-    \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
+    \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
+    \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
     \verb!\end{tabular}!\\
     \verb!\end{center}!
   \end{quote}