Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
changeset 72302 d7d90ed4c74e
parent 68707 5b269897df9d 
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -294,7 +294,7 @@
   have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC"
     unfolding B_def C_def BuC_def by fastforce+
   then show ?thesis
-    unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
+    unfolding b_def c_def using card.empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
 qed
 
 definition f_2:: "int \<Rightarrow> int"
isabelle