# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1340125092 -3600
# Node ID e2c0138b5ceae01e6210c4c0a96faea3e86eccc9
# Parent  efe63c062e48093e8ed65c6781b7832e46387402
polished

diff -r efe63c062e48 -r e2c0138b5cea ProgTutorial/Recipes/Introspection.thy
--- 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
 
diff -r efe63c062e48 -r e2c0138b5cea progtutorial.pdf
Binary file progtutorial.pdf has changed