src/HOL/Datatype.thy
changeset 45607 16b4f5774621
parent 42163 392fd6c4669c
child 45694 4a8743618257
     1.1 --- a/src/HOL/Datatype.thy	Sun Nov 20 21:07:06 2011 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Sun Nov 20 21:07:10 2011 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4  lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
     1.5  by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
     1.6  
     1.7 -lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
     1.8 +lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
     1.9  
    1.10  
    1.11  (*** Introduction rules for Node ***)
    1.12 @@ -155,7 +155,7 @@
    1.13           dest!: Abs_Node_inj 
    1.14           elim!: apfst_convE sym [THEN Push_neq_K0])  
    1.15  
    1.16 -lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
    1.17 +lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
    1.18  
    1.19  
    1.20  (*** Injectiveness ***)
    1.21 @@ -166,7 +166,7 @@
    1.22  apply (simp add: Atom_def)
    1.23  apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
    1.24  done
    1.25 -lemmas Atom_inject = inj_Atom [THEN injD, standard]
    1.26 +lemmas Atom_inject = inj_Atom [THEN injD]
    1.27  
    1.28  lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
    1.29  by (blast dest!: Atom_inject)
    1.30 @@ -177,7 +177,7 @@
    1.31  apply (erule Atom_inject [THEN Inl_inject])
    1.32  done
    1.33  
    1.34 -lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard]
    1.35 +lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
    1.36  
    1.37  lemma inj_Numb: "inj(Numb)"
    1.38  apply (simp add: Numb_def o_def)
    1.39 @@ -185,7 +185,7 @@
    1.40  apply (erule Atom_inject [THEN Inr_inject])
    1.41  done
    1.42  
    1.43 -lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard]
    1.44 +lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
    1.45  
    1.46  
    1.47  (** Injectiveness of Push_Node **)
    1.48 @@ -235,14 +235,14 @@
    1.49  lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
    1.50  unfolding Leaf_def o_def by (rule Scons_not_Atom)
    1.51  
    1.52 -lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
    1.53 +lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
    1.54  
    1.55  (** Scons vs Numb **)
    1.56  
    1.57  lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
    1.58  unfolding Numb_def o_def by (rule Scons_not_Atom)
    1.59  
    1.60 -lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
    1.61 +lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
    1.62  
    1.63  
    1.64  (** Leaf vs Numb **)
    1.65 @@ -250,7 +250,7 @@
    1.66  lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
    1.67  by (simp add: Leaf_def Numb_def)
    1.68  
    1.69 -lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard]
    1.70 +lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
    1.71  
    1.72  
    1.73  (*** ndepth -- the depth of a node ***)
    1.74 @@ -357,7 +357,7 @@
    1.75  lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
    1.76  unfolding In0_def In1_def One_nat_def by auto
    1.77  
    1.78 -lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
    1.79 +lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
    1.80  
    1.81  lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
    1.82  by (simp add: In0_def)
    1.83 @@ -503,7 +503,7 @@
    1.84  lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
    1.85  by blast
    1.86  
    1.87 -lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard]
    1.88 +lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
    1.89  
    1.90  (*Dependent version*)
    1.91  lemma dprod_subset_Sigma2:
    1.92 @@ -514,7 +514,7 @@
    1.93  lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
    1.94  by blast
    1.95  
    1.96 -lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
    1.97 +lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
    1.98  
    1.99  
   1.100  text {* hides popular names *}