# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1238741707 -3600
# Node ID fe45fbb111c55f016e6d3a115e5440cc66506f35
# Parent  a00c7721fc3b2f2d93a598c0f613524c22f1b8c0
various additions

diff -r a00c7721fc3b -r fe45fbb111c5 IsaMakefile
--- a/IsaMakefile	Thu Apr 02 12:19:11 2009 +0100
+++ b/IsaMakefile	Fri Apr 03 07:55:07 2009 +0100
@@ -29,6 +29,7 @@
           ProgTutorial/Package/*.ML 
 	$(USEDIR) HOL ProgTutorial
 	$(ISATOOL) version > ProgTutorial/generated/version 
+	poly -v > ProgTutorial/generated/pversion
 	$(ISATOOL) document -o pdf  ProgTutorial/generated
 	@cp ProgTutorial/document.pdf progtutorial.pdf
 
diff -r a00c7721fc3b -r fe45fbb111c5 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Thu Apr 02 12:19:11 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Fri Apr 03 07:55:07 2009 +0100
@@ -732,7 +732,7 @@
   "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
-  In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}), 
+  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}), 
   and an abstraction. It also records the type of the abstracted
   variable and for printing purposes also its name.  Note that because of the
   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
diff -r a00c7721fc3b -r fe45fbb111c5 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Thu Apr 02 12:19:11 2009 +0100
+++ b/ProgTutorial/Intro.thy	Fri Apr 03 07:55:07 2009 +0100
@@ -161,7 +161,8 @@
   
   \vfill
   This document was compiled with:\\
-  \input{version}
+  \input{version}\\
+  \input{pversion}
 *}
 
 
diff -r a00c7721fc3b -r fe45fbb111c5 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Thu Apr 02 12:19:11 2009 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Fri Apr 03 07:55:07 2009 +0100
@@ -179,6 +179,13 @@
   Write code that automates the derivation of the strong induction 
   principles from the weak ones.
   \end{exercise}
+
+  \begin{readmore}
+  The standard inductive package is based on least fix-points. It allows more 
+  general introduction rules that can include any monotone operators and also
+  provides a richer reasoning infrastructure. The code of this package can be found in 
+  @{ML_file "HOL/Tools/inductive_package.ML"}.
+  \end{readmore}
 *}
 
 
diff -r a00c7721fc3b -r fe45fbb111c5 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Thu Apr 02 12:19:11 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Fri Apr 03 07:55:07 2009 +0100
@@ -618,14 +618,12 @@
   for inductive predicates of the form:
 *}
 
-(*
 simple_inductive
   even and odd
 where
   even0: "even 0"
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
-*)
 
 text {*
   For this we are going to use the parser:
diff -r a00c7721fc3b -r fe45fbb111c5 progtutorial.pdf
Binary file progtutorial.pdf has changed