Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
authorwenzelm
Fri, 25 Nov 2011 13:14:58 +0100
changeset 45630 0dd654a01217
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 file | annotate | diff | comparison | revisions
src/HOL/Predicate.thy file | annotate | diff | comparison | revisions 
--- 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"
--- 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"
isabelle