--- a/src/HOL/Datatype.thy Sat Nov 18 00:20:12 2006 +0100
+++ b/src/HOL/Datatype.thy Sat Nov 18 00:20:13 2006 +0100
@@ -155,8 +155,8 @@
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 ***)
@@ -177,8 +177,7 @@
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)
@@ -186,8 +185,7 @@
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 **)
@@ -239,16 +237,14 @@
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 **)
@@ -256,8 +252,7 @@
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 ***)
@@ -363,8 +358,7 @@
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)