--- a/ProgTutorial/Recipes/Introspection.thy	Tue Jun 19 17:27:10 2012 +0100
+++ b/ProgTutorial/Recipes/Introspection.thy	Tue Jun 19 17:58:12 2012 +0100
@@ -12,7 +12,7 @@
   {\bf Solution:} They can be obtained by introspecting the theorem.\smallskip
 
   To introspect a theorem, let us define the following three functions that 
-  analyse the @{ML_type proof_body} data-structure from the structure 
+  analyse the @{ML_type_ind proof_body} data-structure from the structure 
   @{ML_struct Proofterm}.
 *}
 
@@ -25,7 +25,7 @@
 *}
 
 lemma my_conjIa:
-  shows "A \<and> B \<Longrightarrow> A \<and> B"
+shows "A \<and> B \<Longrightarrow> A \<and> B"
 apply(rule conjI)
 apply(drule conjunct1)
 apply(assumption)
@@ -34,12 +34,12 @@
 done
 
 lemma my_conjIb:
-  shows "A \<and> B \<Longrightarrow> A \<and> B"
+shows "A \<and> B \<Longrightarrow> A \<and> B"
 apply(assumption)
 done
 
 lemma my_conjIc:
-  shows "A \<and> B \<Longrightarrow> A \<and> B"
+shows "A \<and> B \<Longrightarrow> A \<and> B"
 apply(auto)
 done
 

Binary file progtutorial.pdf has changed