1.1 --- a/src/ZF/Induct/Binary_Trees.thy	Tue Mar 13 14:17:42 2012 +0100
     1.2 +++ b/src/ZF/Induct/Binary_Trees.thy	Tue Mar 13 14:44:16 2012 +0100
     1.3 @@ -123,10 +123,10 @@
     1.4  *}
     1.5  
     1.6  lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
     1.7 -  by (induct set: bt) (simp_all add: add_commute n_leaves_type)
     1.8 +  by (induct set: bt) (simp_all add: add_commute)
     1.9  
    1.10  lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
    1.11 -  by (induct set: bt) (simp_all add: add_succ_right)
    1.12 +  by (induct set: bt) simp_all
    1.13  
    1.14  text {*
    1.15    Theorems about @{term bt_reflect}.

     2.1 --- a/src/ZF/Induct/Brouwer.thy	Tue Mar 13 14:17:42 2012 +0100
     2.2 +++ b/src/ZF/Induct/Brouwer.thy	Tue Mar 13 14:44:16 2012 +0100
     2.3 @@ -71,7 +71,7 @@
     2.4    -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
     2.5    -- {* for @{text Well} to prove this. *}
     2.6    apply (rule Well_unfold [THEN trans])
     2.7 -  apply (simp add: Sigma_bool Pi_empty1 succ_def)
     2.8 +  apply (simp add: Sigma_bool succ_def)
     2.9    done
    2.10  
    2.11  end

     3.1 --- a/src/ZF/Induct/Comb.thy	Tue Mar 13 14:17:42 2012 +0100
     3.2 +++ b/src/ZF/Induct/Comb.thy	Tue Mar 13 14:44:16 2012 +0100
     3.3 @@ -114,8 +114,6 @@
     3.4  
     3.5  inductive_cases Ap_E [elim!]: "p\<bullet>q \<in> comb"
     3.6  
     3.7 -declare comb.intros [intro!]
     3.8 -
     3.9  
    3.10  subsection {* Results about Contraction *}
    3.11  
    3.12 @@ -189,13 +187,13 @@
    3.13  text {* Counterexample to the diamond property for @{text "-1->"}. *}
    3.14  
    3.15  lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
    3.16 -  by (blast intro: comb.intros contract.K comb_I)
    3.17 +  by (blast intro: comb_I)
    3.18  
    3.19  lemma KIII_contract2: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I))"
    3.20 -  by (unfold I_def) (blast intro: comb.intros contract.intros)
    3.21 +  by (unfold I_def) (blast intro: contract.intros)
    3.22  
    3.23  lemma KIII_contract3: "K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I)) -1-> I"
    3.24 -  by (blast intro: comb.intros contract.K comb_I)
    3.25 +  by (blast intro: comb_I)
    3.26  
    3.27  lemma not_diamond_contract: "\<not> diamond(contract)"
    3.28    apply (unfold diamond_def)

     4.1 --- a/src/ZF/Induct/Term.thy	Tue Mar 13 14:17:42 2012 +0100
     4.2 +++ b/src/ZF/Induct/Term.thy	Tue Mar 13 14:44:16 2012 +0100
     4.3 @@ -138,8 +138,7 @@
     4.4    apply (subst term_rec)
     4.5     apply (assumption | rule a)+
     4.6    apply (erule list.induct)
     4.7 -   apply (simp add: term_rec)
     4.8 -  apply (auto simp add: term_rec)
     4.9 +   apply auto
    4.10    done
    4.11  
    4.12  lemma def_term_rec: