--- 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}.
--- 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
--- 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)
--- 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: