# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1413412805 -3600
# Node ID 8d30446d89f022e59bfe83fd133cc87c8b76dd36
# Parent  ffa5c4ec9611ae2bc03df5a5a63b7905cc254e4e
updated to new Isabelle

diff -r ffa5c4ec9611 -r 8d30446d89f0 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Wed Oct 15 23:12:54 2014 +0100
+++ b/ProgTutorial/Advanced.thy	Wed Oct 15 23:40:05 2014 +0100
@@ -574,8 +574,6 @@
 
 section {* Misc (TBD) *}
 
-ML {*Datatype.get_info @{theory} "List.list"*}
-
 text {* 
 FIXME: association lists:
 @{ML_file "Pure/General/alist.ML"}
diff -r ffa5c4ec9611 -r 8d30446d89f0 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Wed Oct 15 23:12:54 2014 +0100
+++ b/ProgTutorial/Intro.thy	Wed Oct 15 23:40:05 2014 +0100
@@ -321,6 +321,8 @@
 
   \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
   @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. 
+
+  \item {\bf Piotr Trojanek} proofread the text.
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining
diff -r ffa5c4ec9611 -r 8d30446d89f0 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Wed Oct 15 23:12:54 2014 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Wed Oct 15 23:40:05 2014 +0100
@@ -207,10 +207,6 @@
 
 datatype foo = Foo nat
 
-local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] 
-    [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})]
-  #> snd *}
-
 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
     [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
       conf pat_completeness_auto #> snd*}
diff -r ffa5c4ec9611 -r 8d30446d89f0 progtutorial.pdf
Binary file progtutorial.pdf has changed