src/HOL/Datatype.thy

 apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
          dest!: Abs_Node_inj 
          elim!: apfst_convE sym [THEN Push_neq_K0])  
 done
 
-lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard]
-declare Atom_not_Scons [iff]
+lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
+
 
 (*** Injectiveness ***)
 
 (** Atomic nodes **)
 

 apply (simp add: Leaf_def o_def)
 apply (rule inj_onI)
 apply (erule Atom_inject [THEN Inl_inject])
 done
 
-lemmas Leaf_inject = inj_Leaf [THEN injD, standard]
-declare Leaf_inject [dest!]
+lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard]
 
 lemma inj_Numb: "inj(Numb)"
 apply (simp add: Numb_def o_def)
 apply (rule inj_onI)
 apply (erule Atom_inject [THEN Inr_inject])
 done
 
-lemmas Numb_inject = inj_Numb [THEN injD, standard]
-declare Numb_inject [dest!]
+lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard]
 
 
 (** Injectiveness of Push_Node **)
 
 lemma Push_Node_inject:

 (** Scons vs Leaf **)
 
 lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
 by (simp add: Leaf_def o_def Scons_not_Atom)
 
-lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard]
-declare Leaf_not_Scons [iff]
+lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
 
 (** Scons vs Numb **)
 
 lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
 by (simp add: Numb_def o_def Scons_not_Atom)
 
-lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard]
-declare Numb_not_Scons [iff]
+lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
 
 
 (** Leaf vs Numb **)
 
 lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
 by (simp add: Leaf_def Numb_def)
 
-lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard]
-declare Numb_not_Leaf [iff]
+lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard]
 
 
 (*** ndepth -- the depth of a node ***)
 
 lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"

 (** Injection **)
 
 lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
 by (auto simp add: In0_def In1_def One_nat_def)
 
-lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard]
-declare In1_not_In0 [iff]
+lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
 
 lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
 by (simp add: In0_def)
 
 lemma In1_inject: "In1(M) = In1(N) ==>  M=N"