eliminated obsolete "standard";
authorwenzelm
Sun Nov 20 21:28:07 2011 +0100 (2011-11-20)
changeset 4560813b101cee425
parent 45607 16b4f5774621
child 45609 2c0c8ce96f4a
eliminated obsolete "standard";
src/HOL/Bali/WellForm.thy
src/HOL/Library/Multiset.thy
src/ZF/Arith.thy
     1.1 --- a/src/HOL/Bali/WellForm.thy	Sun Nov 20 21:07:10 2011 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Sun Nov 20 21:28:07 2011 +0100
     1.3 @@ -733,13 +733,14 @@
     1.4   \<Longrightarrow> declclass m = Object"
     1.5  by (auto dest: class_Object simp add: methd_rec )
     1.6  
     1.7 +lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P
     1.8 +
     1.9  lemma wf_imethdsD: 
    1.10   "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
    1.11   \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
    1.12  proof -
    1.13    assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
    1.14  
    1.15 -  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]  (* FIXME !? *)
    1.16    have "wf_prog G \<longrightarrow> 
    1.17           (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
    1.18                    \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
     2.1 --- a/src/HOL/Library/Multiset.thy	Sun Nov 20 21:07:10 2011 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Sun Nov 20 21:28:07 2011 +0100
     2.3 @@ -1527,7 +1527,7 @@
     2.4  apply (rule iffI)
     2.5   prefer 2
     2.6   apply blast
     2.7 -apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard])
     2.8 +apply (rule_tac A1=A and f1=f in fold_msetG_nonempty [THEN exE])
     2.9  apply (blast intro: fold_msetG_determ)
    2.10  done
    2.11  
     3.1 --- a/src/ZF/Arith.thy	Sun Nov 20 21:07:10 2011 +0100
     3.2 +++ b/src/ZF/Arith.thy	Sun Nov 20 21:28:07 2011 +0100
     3.3 @@ -88,7 +88,7 @@
     3.4  done
     3.5  
     3.6  (* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *)
     3.7 -lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
     3.8 +lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
     3.9  
    3.10  
    3.11  subsection{*@{text natify}, the Coercion to @{term nat}*}