src/HOL/Datatype.thy
changeset 21407 af60523da908
parent 21404 eb85850d3eb7
child 21454 a1937c51ed88
     1.1 --- a/src/HOL/Datatype.thy	Sat Nov 18 00:20:12 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Sat Nov 18 00:20:13 2006 +0100
     1.3 @@ -155,8 +155,8 @@
     1.4           elim!: apfst_convE sym [THEN Push_neq_K0])  
     1.5  done
     1.6  
     1.7 -lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard]
     1.8 -declare Atom_not_Scons [iff]
     1.9 +lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
    1.10 +
    1.11  
    1.12  (*** Injectiveness ***)
    1.13  
    1.14 @@ -177,8 +177,7 @@
    1.15  apply (erule Atom_inject [THEN Inl_inject])
    1.16  done
    1.17  
    1.18 -lemmas Leaf_inject = inj_Leaf [THEN injD, standard]
    1.19 -declare Leaf_inject [dest!]
    1.20 +lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard]
    1.21  
    1.22  lemma inj_Numb: "inj(Numb)"
    1.23  apply (simp add: Numb_def o_def)
    1.24 @@ -186,8 +185,7 @@
    1.25  apply (erule Atom_inject [THEN Inr_inject])
    1.26  done
    1.27  
    1.28 -lemmas Numb_inject = inj_Numb [THEN injD, standard]
    1.29 -declare Numb_inject [dest!]
    1.30 +lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard]
    1.31  
    1.32  
    1.33  (** Injectiveness of Push_Node **)
    1.34 @@ -239,16 +237,14 @@
    1.35  lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
    1.36  by (simp add: Leaf_def o_def Scons_not_Atom)
    1.37  
    1.38 -lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard]
    1.39 -declare Leaf_not_Scons [iff]
    1.40 +lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
    1.41  
    1.42  (** Scons vs Numb **)
    1.43  
    1.44  lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
    1.45  by (simp add: Numb_def o_def Scons_not_Atom)
    1.46  
    1.47 -lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard]
    1.48 -declare Numb_not_Scons [iff]
    1.49 +lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
    1.50  
    1.51  
    1.52  (** Leaf vs Numb **)
    1.53 @@ -256,8 +252,7 @@
    1.54  lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
    1.55  by (simp add: Leaf_def Numb_def)
    1.56  
    1.57 -lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard]
    1.58 -declare Numb_not_Leaf [iff]
    1.59 +lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard]
    1.60  
    1.61  
    1.62  (*** ndepth -- the depth of a node ***)
    1.63 @@ -363,8 +358,7 @@
    1.64  lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
    1.65  by (auto simp add: In0_def In1_def One_nat_def)
    1.66  
    1.67 -lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard]
    1.68 -declare In1_not_In0 [iff]
    1.69 +lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
    1.70  
    1.71  lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
    1.72  by (simp add: In0_def)