# HG changeset patch
# User wenzelm
# Date 1331646256 -3600
# Node ID 73555abfa267fad331ced96bfa9d108a45c298b6
# Parent  58110c1e02bcd35412002ad319c0f60ee0dd9dc0
tuned proofs;

diff -r 58110c1e02bc -r 73555abfa267 src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -123,10 +123,10 @@
 *}
 
 lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
-  by (induct set: bt) (simp_all add: add_commute n_leaves_type)
+  by (induct set: bt) (simp_all add: add_commute)
 
 lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
-  by (induct set: bt) (simp_all add: add_succ_right)
+  by (induct set: bt) simp_all
 
 text {*
   Theorems about @{term bt_reflect}.
diff -r 58110c1e02bc -r 73555abfa267 src/ZF/Induct/Brouwer.thy
--- a/src/ZF/Induct/Brouwer.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -71,7 +71,7 @@
   -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
   -- {* for @{text Well} to prove this. *}
   apply (rule Well_unfold [THEN trans])
-  apply (simp add: Sigma_bool Pi_empty1 succ_def)
+  apply (simp add: Sigma_bool succ_def)
   done
 
 end
diff -r 58110c1e02bc -r 73555abfa267 src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Comb.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -114,8 +114,6 @@
 
 inductive_cases Ap_E [elim!]: "p\<bullet>q \<in> comb"
 
-declare comb.intros [intro!]
-
 
 subsection {* Results about Contraction *}
 
@@ -189,13 +187,13 @@
 text {* Counterexample to the diamond property for @{text "-1->"}. *}
 
 lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
-  by (blast intro: comb.intros contract.K comb_I)
+  by (blast intro: comb_I)
 
 lemma KIII_contract2: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I))"
-  by (unfold I_def) (blast intro: comb.intros contract.intros)
+  by (unfold I_def) (blast intro: contract.intros)
 
 lemma KIII_contract3: "K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I)) -1-> I"
-  by (blast intro: comb.intros contract.K comb_I)
+  by (blast intro: comb_I)
 
 lemma not_diamond_contract: "\<not> diamond(contract)"
   apply (unfold diamond_def)
diff -r 58110c1e02bc -r 73555abfa267 src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Term.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -138,8 +138,7 @@
   apply (subst term_rec)
    apply (assumption | rule a)+
   apply (erule list.induct)
-   apply (simp add: term_rec)
-  apply (auto simp add: term_rec)
+   apply auto
   done
 
 lemma def_term_rec: