--- a/src/ZF/Bin.thy Thu Nov 07 15:30:48 2019 +0100
+++ b/src/ZF/Bin.thy Thu Nov 07 16:03:26 2019 +0100
@@ -162,7 +162,7 @@
by (induct_tac "w", auto)
(*This proof is complicated by the mutual recursion*)
-lemma bin_add_type [rule_format,TC]:
+lemma bin_add_type [rule_format]:
"v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
apply (unfold bin_add_def)
apply (induct_tac "v")
@@ -172,6 +172,8 @@
apply (simp_all add: NCons_type)
done
+declare bin_add_type [TC]
+
lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin"
by (induct_tac "v", auto)