proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
authorwenzelm
Fri Nov 25 13:14:58 2011 +0100 (2011-11-25)
changeset 456300dd654a01217
parent 45629 ef08425dd2d5
child 45631 6bdf8b926f50
proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 10:52:30 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 13:14:58 2011 +0100
     1.3 @@ -114,8 +114,8 @@
     1.4     (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
     1.5  proof -
     1.6    assume "a \<in> zOdd"
     1.7 -  from QRLemma4 [OF this, symmetric] have
     1.8 -    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
     1.9 +  from QRLemma4 [OF this] have
    1.10 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
    1.11    moreover have "0 \<le> int(card E)"
    1.12      by auto
    1.13    moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
     2.1 --- a/src/HOL/Predicate.thy	Fri Nov 25 10:52:30 2011 +0100
     2.2 +++ b/src/HOL/Predicate.thy	Fri Nov 25 13:14:58 2011 +0100
     2.3 @@ -145,16 +145,16 @@
     2.4  
     2.5  subsubsection {* Binary union *}
     2.6  
     2.7 -lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
     2.8 +lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
     2.9    by (simp add: sup_fun_def)
    2.10  
    2.11 -lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
    2.12 +lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
    2.13    by (simp add: sup_fun_def)
    2.14  
    2.15 -lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
    2.16 +lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
    2.17    by (simp add: sup_fun_def)
    2.18  
    2.19 -lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
    2.20 +lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
    2.21    by (simp add: sup_fun_def)
    2.22  
    2.23  lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"