--- a/ProgTutorial/Solutions.thy	Fri Aug 13 18:42:58 2010 +0800
+++ b/ProgTutorial/Solutions.thy	Fri Aug 13 18:52:16 2010 +0800
@@ -14,8 +14,8 @@
 
 text {* \solution{fun:revsum} *}
 
-ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = 
-      p $ u $ rev_sum t
+ML{*fun rev_sum 
+  ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t
   | rev_sum t = t *}
 
 text {* 
@@ -27,13 +27,13 @@
   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
     | dest_sum u = [u]
 in
-   foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
+  foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 end *}
 
 text {* \solution{fun:makesum} *}
 
 ML{*fun make_sum t1 t2 =
-      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
+  HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
 
 text {* \solution{fun:makelist} *}
@@ -143,19 +143,10 @@
 
 lemma impE2:
   shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-  by iprover
-
-lemma impE3:
-  shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-  by iprover
-
-lemma impE4:
-  shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-  by iprover
-
-lemma impE5:
-  shows "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
-  by iprover
+  and   "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  and   "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  and   "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by iprover+
 
 text {*
   Now the tactic which applies a single rule can be implemented
@@ -164,10 +155,8 @@
 
 ML %linenosgray{*val apply_tac =
 let
-  val intros = [@{thm conjI}, @{thm disjI1}, @{thm disjI2}, 
-                @{thm impI}, @{thm iffI}]
-  val elims  = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE},
-                @{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}]
+  val intros = @{thms conjI disjI1 disjI2 impI iffI}
+  val elims = @{thms FalseE conjE disjE iffE impE2}
 in
   atac
   ORELSE' resolve_tac intros