# HG changeset patch
# User wenzelm
# Date 1322223298 -3600
# Node ID 0dd654a01217090b06bc70ff0bc2b78f15df77e0
# Parent  ef08425dd2d5c72fae6eddb72f2deb0ed48848c7
proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

diff -r ef08425dd2d5 -r 0dd654a01217 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 10:52:30 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 13:14:58 2011 +0100
@@ -114,8 +114,8 @@
    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
 proof -
   assume "a \<in> zOdd"
-  from QRLemma4 [OF this, symmetric] have
-    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
+  from QRLemma4 [OF this] have
+    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
   moreover have "0 \<le> int(card E)"
     by auto
   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
diff -r ef08425dd2d5 -r 0dd654a01217 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Nov 25 10:52:30 2011 +0100
+++ b/src/HOL/Predicate.thy	Fri Nov 25 13:14:58 2011 +0100
@@ -145,16 +145,16 @@
 
 subsubsection {* Binary union *}
 
-lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
+lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
 
-lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
+lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   by (simp add: sup_fun_def)
 
-lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
+lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
 
-lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
+lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   by (simp add: sup_fun_def)
 
 lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"