src/HOL/Datatype.thy

 by (blast dest: Push_inject1 Push_inject2) 
 
 lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
 by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
 
-lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
+lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
 
 
 (*** Introduction rules for Node ***)
 
 lemma Node_K0_I: "(%k. Inr 0, a) : Node"

 unfolding Atom_def Scons_def Push_Node_def One_nat_def
 by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
          dest!: Abs_Node_inj 
          elim!: apfst_convE sym [THEN Push_neq_K0])  
 
-lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
+lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
 
 
 (*** Injectiveness ***)
 
 (** Atomic nodes **)
 
 lemma inj_Atom: "inj(Atom)"
 apply (simp add: Atom_def)
 apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
 done
-lemmas Atom_inject = inj_Atom [THEN injD, standard]
+lemmas Atom_inject = inj_Atom [THEN injD]
 
 lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
 by (blast dest!: Atom_inject)
 
 lemma inj_Leaf: "inj(Leaf)"
 apply (simp add: Leaf_def o_def)
 apply (rule inj_onI)
 apply (erule Atom_inject [THEN Inl_inject])
 done
 
-lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard]
+lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
 
 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 [dest!] = inj_Numb [THEN injD, standard]
+lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
 
 
 (** Injectiveness of Push_Node **)
 
 lemma Push_Node_inject:

 (** Scons vs Leaf **)
 
 lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
 unfolding Leaf_def o_def by (rule Scons_not_Atom)
 
-lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
+lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
 
 (** Scons vs Numb **)
 
 lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
 unfolding Numb_def o_def by (rule Scons_not_Atom)
 
-lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
+lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
 
 
 (** Leaf vs Numb **)
 
 lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
 by (simp add: Leaf_def Numb_def)
 
-lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard]
+lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
 
 
 (*** 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)"
 unfolding In0_def In1_def One_nat_def by auto
 
-lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
+lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
 
 lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
 by (simp add: In0_def)
 
 lemma In1_inject: "In1(M) = In1(N) ==>  M=N"

 (*** Bounding theorems ***)
 
 lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
 by blast
 
-lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard]
+lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
 
 (*Dependent version*)
 lemma dprod_subset_Sigma2:
      "(dprod (Sigma A B) (Sigma C D)) <= 
       Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
 by auto
 
 lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
 by blast
 
-lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
+lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
 
 
 text {* hides popular names *}
 hide_type (open) node item
 hide_const (open) Push Node Atom Leaf Numb Lim Split Case