# HG changeset patch
# User haftmann
# Date 1163805613 -3600
# Node ID af60523da9088daa43d34efaa8755719e7320f3d
# Parent  4058f08864487f877157acc28ce9e4f0f4465553
reduced verbosity

diff -r 4058f0886448 -r af60523da908 src/HOL/Datatype.thy
--- 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)