added IntGroup_ZF to theories parsed for isarmathlib.org

SKolodynski · Dec 25, 2024 · c6cdaa4 · c6cdaa4
1 parent 51169e8
commit c6cdaa4
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 2 deletions.
diff --git a/IsarMathLib/InductiveSeq_ZF.thy b/IsarMathLib/InductiveSeq_ZF.thy
@@ -1145,7 +1145,7 @@ proof -
   ultimately have "?B(n,n #+ 1) = 0"
     unfolding Binom_def by simp
   with assms \<open>?B(n,n) \<in> nat\<close> show ?thesis
-    using succ_add_one(2) binom_prop add_subctract add_0 add_commute
+    using succ_add_one(2) binom_prop add_subtract add_0 add_commute
     by simp
 qed
 

diff --git a/IsarMathLib/IntGroup_ZF.thy b/IsarMathLib/IntGroup_ZF.thy
@@ -259,7 +259,7 @@ lemma (in group_int0) powz_hom_neg_nneg2:
   by simp
 
 text\<open>The next theorem collects the results from the above lemmas to show
-  the power homomorphism property hols for any pair of integer numbers
+  the power homomorphism property holds for any pair of integer numbers
   and any group element. \<close>
 
 theorem (in group_int0) powz_hom_prop: assumes "z\<^sub>1\<in>\<int>" "z\<^sub>2\<in>\<int>" "x\<in>G"

diff --git a/isar2html2.0/isarhtml/index.html b/isar2html2.0/isarhtml/index.html
@@ -187,6 +187,8 @@ <h3>About this site</h3>
 
 <p><a href="Int_ZF_3.html">Int_ZF_3</a></p>
 
+<p><a href="IntGroup_ZF.html">Int_ZF_3</a></p>
+
 <p><a href="Real_ZF.html">Real_ZF</a></p>
 
 <p><a href="Real_ZF_1.html">Real_ZF_1</a></p>

diff --git a/isar2html2.0/theories.conf b/isar2html2.0/theories.conf
@@ -55,6 +55,7 @@ Int_ZF_1
 IntDiv_ZF_IML
 Int_ZF_2
 Int_ZF_3
+IntGroup_ZF
 Real_ZF
 Real_ZF_1
 Complex_ZF