Merge pull request #213 from daviddoret/dev

Dev
daviddoret · Sep 21, 2023 · 33c23b1 · 33c23b1
2 parents bca7caf + 7413a28
commit 33c23b1
Show file tree

Hide file tree

Showing 351 changed files with 2,062 additions and 1,606 deletions.
diff --git a/.idea/workspace.xml b/.idea/workspace.xml
diff --git a/_build/doctrees/_tags/absorption.doctree b/_build/doctrees/_tags/absorption.doctree
diff --git a/_build/doctrees/_tags/biconditional-elimination-1.doctree b/_build/doctrees/_tags/biconditional-elimination-1.doctree
diff --git a/_build/doctrees/_tags/biconditional-elimination-2.doctree b/_build/doctrees/_tags/biconditional-elimination-2.doctree
diff --git a/_build/doctrees/_tags/biconditional-introduction.doctree b/_build/doctrees/_tags/biconditional-introduction.doctree
diff --git a/_build/doctrees/_tags/class.doctree b/_build/doctrees/_tags/class.doctree
diff --git a/_build/doctrees/_tags/concept.doctree b/_build/doctrees/_tags/concept.doctree
diff --git a/_build/doctrees/_tags/conjunction-elimination-1.doctree b/_build/doctrees/_tags/conjunction-elimination-1.doctree
diff --git a/_build/doctrees/_tags/conjunction-elimination-2.doctree b/_build/doctrees/_tags/conjunction-elimination-2.doctree
diff --git a/_build/doctrees/_tags/conjunction-introduction.doctree b/_build/doctrees/_tags/conjunction-introduction.doctree
diff --git a/_build/doctrees/_tags/declaration.doctree b/_build/doctrees/_tags/declaration.doctree
diff --git a/_build/doctrees/_tags/disjunction-introduction-1.doctree b/_build/doctrees/_tags/disjunction-introduction-1.doctree
diff --git a/_build/doctrees/_tags/disjunction-introduction-2.doctree b/_build/doctrees/_tags/disjunction-introduction-2.doctree
diff --git a/_build/doctrees/_tags/double-negation-elimination.doctree b/_build/doctrees/_tags/double-negation-elimination.doctree
diff --git a/_build/doctrees/_tags/double-negation-introduction.doctree b/_build/doctrees/_tags/double-negation-introduction.doctree
diff --git a/_build/doctrees/_tags/equal-terms-substitution.doctree b/_build/doctrees/_tags/equal-terms-substitution.doctree
diff --git a/_build/doctrees/_tags/equality-commutativity.doctree b/_build/doctrees/_tags/equality-commutativity.doctree
diff --git a/_build/doctrees/_tags/inclusion.doctree b/_build/doctrees/_tags/inclusion.doctree
diff --git a/_build/doctrees/_tags/inconsistency-introduction-1.doctree b/_build/doctrees/_tags/inconsistency-introduction-1.doctree
diff --git a/_build/doctrees/_tags/inconsistency-introduction-2.doctree b/_build/doctrees/_tags/inconsistency-introduction-2.doctree
diff --git a/_build/doctrees/_tags/inconsistency-introduction-3.doctree b/_build/doctrees/_tags/inconsistency-introduction-3.doctree
diff --git a/_build/doctrees/_tags/inference-rule.doctree b/_build/doctrees/_tags/inference-rule.doctree
diff --git a/_build/doctrees/_tags/math.doctree b/_build/doctrees/_tags/math.doctree
diff --git a/_build/doctrees/_tags/modus-ponens.doctree b/_build/doctrees/_tags/modus-ponens.doctree
diff --git a/_build/doctrees/_tags/proof-by-contradiction-1.doctree b/_build/doctrees/_tags/proof-by-contradiction-1.doctree
diff --git a/_build/doctrees/_tags/proof-by-contradiction-2.doctree b/_build/doctrees/_tags/proof-by-contradiction-2.doctree
diff --git a/_build/doctrees/_tags/proof-by-refutation-1.doctree b/_build/doctrees/_tags/proof-by-refutation-1.doctree
diff --git a/_build/doctrees/_tags/proof-by-refutation-2.doctree b/_build/doctrees/_tags/proof-by-refutation-2.doctree
diff --git a/_build/doctrees/_tags/python.doctree b/_build/doctrees/_tags/python.doctree
diff --git a/_build/doctrees/_tags/sample.doctree b/_build/doctrees/_tags/sample.doctree
diff --git a/_build/doctrees/_tags/tagsindex.doctree b/_build/doctrees/_tags/tagsindex.doctree
diff --git a/_build/doctrees/_tags/universe-of-discourse.doctree b/_build/doctrees/_tags/universe-of-discourse.doctree
diff --git a/_build/doctrees/_tags/variable-substitution.doctree b/_build/doctrees/_tags/variable-substitution.doctree
diff --git a/_build/doctrees/back_matter.doctree b/_build/doctrees/back_matter.doctree
diff --git a/_build/doctrees/back_matter/bibliography_back_matter.doctree b/_build/doctrees/back_matter/bibliography_back_matter.doctree
diff --git a/_build/doctrees/environment.pickle b/_build/doctrees/environment.pickle
diff --git a/_build/doctrees/front_matter.doctree b/_build/doctrees/front_matter.doctree
diff --git a/_build/doctrees/front_matter/about_front_matter.doctree b/_build/doctrees/front_matter/about_front_matter.doctree
diff --git a/_build/doctrees/front_matter/contributing_front_matter.doctree b/_build/doctrees/front_matter/contributing_front_matter.doctree
diff --git a/_build/doctrees/front_matter/project_front_matter.doctree b/_build/doctrees/front_matter/project_front_matter.doctree
diff --git a/_build/doctrees/front_matter/roadmap_front_matter.doctree b/_build/doctrees/front_matter/roadmap_front_matter.doctree
diff --git a/_build/doctrees/front_matter/support_front_matter.doctree b/_build/doctrees/front_matter/support_front_matter.doctree
diff --git a/_build/doctrees/front_matter/title_front_matter.doctree b/_build/doctrees/front_matter/title_front_matter.doctree
diff --git a/_build/doctrees/index.doctree b/_build/doctrees/index.doctree
diff --git a/_build/doctrees/math.doctree b/_build/doctrees/math.doctree
diff --git a/_build/doctrees/math/concept/axiom_math_concept.doctree b/_build/doctrees/math/concept/axiom_math_concept.doctree
diff --git a/_build/doctrees/math/concept/elimination_rule_math_concept.doctree b/_build/doctrees/math/concept/elimination_rule_math_concept.doctree
diff --git a/_build/doctrees/math/concept/formula_math_concept.doctree b/_build/doctrees/math/concept/formula_math_concept.doctree
diff --git a/_build/doctrees/math/concept/formula_statement_math_concept.doctree b/_build/doctrees/math/concept/formula_statement_math_concept.doctree
diff --git a/_build/doctrees/math/concept/free_variable_math_concept.doctree b/_build/doctrees/math/concept/free_variable_math_concept.doctree
diff --git a/_build/doctrees/math/concept/hypothesis_math_concept.doctree b/_build/doctrees/math/concept/hypothesis_math_concept.doctree
diff --git a/_build/doctrees/math/concept/inference_rule_math_concept.doctree b/_build/doctrees/math/concept/inference_rule_math_concept.doctree
diff --git a/_build/doctrees/math/concept/introduction_rule_math_concept.doctree b/_build/doctrees/math/concept/introduction_rule_math_concept.doctree
diff --git a/_build/doctrees/math/concept/is_a_math_concept.doctree b/_build/doctrees/math/concept/is_a_math_concept.doctree
diff --git a/_build/doctrees/math/concept/meta_object_math_concept.doctree b/_build/doctrees/math/concept/meta_object_math_concept.doctree
diff --git a/_build/doctrees/math/concept/notation_form_math_concept.doctree b/_build/doctrees/math/concept/notation_form_math_concept.doctree
diff --git a/_build/doctrees/math/concept/object_creation_math_concept.doctree b/_build/doctrees/math/concept/object_creation_math_concept.doctree
diff --git a/_build/doctrees/math/concept/object_declaration_math_concept.doctree b/_build/doctrees/math/concept/object_declaration_math_concept.doctree
diff --git a/_build/doctrees/math/concept/object_inclusion_math_concept.doctree b/_build/doctrees/math/concept/object_inclusion_math_concept.doctree
diff --git a/_build/doctrees/math/concept/object_math_concept.doctree b/_build/doctrees/math/concept/object_math_concept.doctree
diff --git a/_build/doctrees/math/concept/paragraph_proof_math_concept.doctree b/_build/doctrees/math/concept/paragraph_proof_math_concept.doctree
diff --git a/_build/doctrees/math/concept/relation_math_concept.doctree b/_build/doctrees/math/concept/relation_math_concept.doctree
diff --git a/_build/doctrees/math/concept/statement_math_concept.doctree b/_build/doctrees/math/concept/statement_math_concept.doctree
diff --git a/_build/doctrees/math/concept/theory_elaboration_sequence_math_concept.doctree b/_build/doctrees/math/concept/theory_elaboration_sequence_math_concept.doctree
diff --git a/_build/doctrees/math/concept/universe_of_discourse_math_concept.doctree b/_build/doctrees/math/concept/universe_of_discourse_math_concept.doctree
diff --git a/_build/doctrees/math/concept/validity_of_formula_math_concept.doctree b/_build/doctrees/math/concept/validity_of_formula_math_concept.doctree
diff --git a/_build/doctrees/math/inference_rule/absorption_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/absorption_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/biconditional_elimination_1_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/biconditional_elimination_1_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/biconditional_elimination_2_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/biconditional_elimination_2_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/biconditional_introduction_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/biconditional_introduction_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/conjunction_elimination_1_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/conjunction_elimination_1_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/conjunction_elimination_2_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/conjunction_elimination_2_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/conjunction_introduction_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/conjunction_introduction_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/disjunction_introduction_1_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/disjunction_introduction_1_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/disjunction_introduction_2_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/disjunction_introduction_2_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/double_negation_elimination_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/double_negation_elimination_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/double_negation_introduction_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/double_negation_introduction_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/equal_terms_substitution_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/equal_terms_substitution_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/equality_commutativity_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/equality_commutativity_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/inconsistency_introduction_1_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/inconsistency_introduction_1_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/inconsistency_introduction_2_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/inconsistency_introduction_2_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/inconsistency_introduction_3_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/inconsistency_introduction_3_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/modus_ponens_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/modus_ponens_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/proof_by_contradiction_1_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/proof_by_contradiction_1_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/proof_by_contradiction_2_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/proof_by_contradiction_2_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/proof_by_refutation_1_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/proof_by_refutation_1_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/proof_by_refutation_2_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/proof_by_refutation_2_math_inference_rule.doctree
diff --git a/_build/doctrees/math/inference_rule/variable_substitution_math_inference_rule.doctree b/_build/doctrees/math/inference_rule/variable_substitution_math_inference_rule.doctree
diff --git a/_build/doctrees/math/theory/tao_2006.doctree b/_build/doctrees/math/theory/tao_2006.doctree
diff --git a/_build/doctrees/math/theory/tao_2006/the_peano_axioms.doctree b/_build/doctrees/math/theory/tao_2006/the_peano_axioms.doctree
diff --git a/_build/doctrees/math_concept.doctree b/_build/doctrees/math_concept.doctree
diff --git a/_build/doctrees/math_inference_rule.doctree b/_build/doctrees/math_inference_rule.doctree
diff --git a/_build/doctrees/math_theory.doctree b/_build/doctrees/math_theory.doctree
diff --git a/_build/doctrees/python.doctree b/_build/doctrees/python.doctree
diff --git a/_build/doctrees/python/class/absorption_declaration_python_class.doctree b/_build/doctrees/python/class/absorption_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/absorption_inclusion_python_class.doctree b/_build/doctrees/python/class/absorption_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/biconditional_elimination_1_declaration_python_class.doctree b/_build/doctrees/python/class/biconditional_elimination_1_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/biconditional_elimination_1_inclusion_python_class.doctree b/_build/doctrees/python/class/biconditional_elimination_1_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/biconditional_elimination_2_declaration_python_class.doctree b/_build/doctrees/python/class/biconditional_elimination_2_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/biconditional_elimination_2_inclusion_python_class.doctree b/_build/doctrees/python/class/biconditional_elimination_2_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/biconditional_introduction_declaration_python_class.doctree b/_build/doctrees/python/class/biconditional_introduction_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/biconditional_introduction_inclusion_python_class.doctree b/_build/doctrees/python/class/biconditional_introduction_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/conjunction_elimination_1_declaration_python_class.doctree b/_build/doctrees/python/class/conjunction_elimination_1_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/conjunction_elimination_1_inclusion_python_class.doctree b/_build/doctrees/python/class/conjunction_elimination_1_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/conjunction_elimination_2_declaration_python_class.doctree b/_build/doctrees/python/class/conjunction_elimination_2_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/conjunction_elimination_2_inclusion_python_class.doctree b/_build/doctrees/python/class/conjunction_elimination_2_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/conjunction_introduction_declaration_python_class.doctree b/_build/doctrees/python/class/conjunction_introduction_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/conjunction_introduction_inclusion_python_class.doctree b/_build/doctrees/python/class/conjunction_introduction_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/disjunction_introduction_1_declaration_python_class.doctree b/_build/doctrees/python/class/disjunction_introduction_1_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/disjunction_introduction_1_inclusion_python_class.doctree b/_build/doctrees/python/class/disjunction_introduction_1_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/disjunction_introduction_2_declaration_python_class.doctree b/_build/doctrees/python/class/disjunction_introduction_2_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/disjunction_introduction_2_inclusion_python_class.doctree b/_build/doctrees/python/class/disjunction_introduction_2_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/double_negation_elimination_declaration_python_class.doctree b/_build/doctrees/python/class/double_negation_elimination_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/double_negation_elimination_inclusion_python_class.doctree b/_build/doctrees/python/class/double_negation_elimination_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/double_negation_introduction_declaration_python_class.doctree b/_build/doctrees/python/class/double_negation_introduction_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/double_negation_introduction_inclusion_python_class.doctree b/_build/doctrees/python/class/double_negation_introduction_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/equal_terms_substitution_declaration_python_class.doctree b/_build/doctrees/python/class/equal_terms_substitution_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/equal_terms_substitution_inclusion_python_class.doctree b/_build/doctrees/python/class/equal_terms_substitution_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/equality_commutativity_declaration_python_class.doctree b/_build/doctrees/python/class/equality_commutativity_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/equality_commutativity_inclusion_python_class.doctree b/_build/doctrees/python/class/equality_commutativity_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/inconsistency_introduction_1_declaration_python_class.doctree b/_build/doctrees/python/class/inconsistency_introduction_1_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/inconsistency_introduction_1_inclusion_python_class.doctree b/_build/doctrees/python/class/inconsistency_introduction_1_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/inconsistency_introduction_2_declaration_python_class.doctree b/_build/doctrees/python/class/inconsistency_introduction_2_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/inconsistency_introduction_2_inclusion_python_class.doctree b/_build/doctrees/python/class/inconsistency_introduction_2_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/inconsistency_introduction_3_declaration_python_class.doctree b/_build/doctrees/python/class/inconsistency_introduction_3_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/inconsistency_introduction_3_inclusion_python_class.doctree b/_build/doctrees/python/class/inconsistency_introduction_3_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/inference_rule_declaration_python_class.doctree b/_build/doctrees/python/class/inference_rule_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/modus_ponens_declaration_python_class.doctree b/_build/doctrees/python/class/modus_ponens_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/modus_ponens_inclusion_python_class.doctree b/_build/doctrees/python/class/modus_ponens_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_contradiction_1_declaration_python_class.doctree b/_build/doctrees/python/class/proof_by_contradiction_1_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_contradiction_1_inclusion_python_class.doctree b/_build/doctrees/python/class/proof_by_contradiction_1_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_contradiction_2_declaration_python_class.doctree b/_build/doctrees/python/class/proof_by_contradiction_2_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_contradiction_2_inclusion_python_class.doctree b/_build/doctrees/python/class/proof_by_contradiction_2_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_refutation_1_declaration_python_class.doctree b/_build/doctrees/python/class/proof_by_refutation_1_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_refutation_1_inclusion_python_class.doctree b/_build/doctrees/python/class/proof_by_refutation_1_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_refutation_2_declaration_python_class.doctree b/_build/doctrees/python/class/proof_by_refutation_2_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/proof_by_refutation_2_inclusion_python_class.doctree b/_build/doctrees/python/class/proof_by_refutation_2_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/class/python_class_index.doctree b/_build/doctrees/python/class/python_class_index.doctree
diff --git a/_build/doctrees/python/class/universe_of_discourse_python_class.doctree b/_build/doctrees/python/class/universe_of_discourse_python_class.doctree
diff --git a/_build/doctrees/python/class/variable_substitution_declaration_python_class.doctree b/_build/doctrees/python/class/variable_substitution_declaration_python_class.doctree
diff --git a/_build/doctrees/python/class/variable_substitution_inclusion_python_class.doctree b/_build/doctrees/python/class/variable_substitution_inclusion_python_class.doctree
diff --git a/_build/doctrees/python/function/create_universe_of_discourse.doctree b/_build/doctrees/python/function/create_universe_of_discourse.doctree
diff --git a/_build/doctrees/python/function/python_function_index.doctree b/_build/doctrees/python/function/python_function_index.doctree
diff --git a/_build/doctrees/python/installation_python.doctree b/_build/doctrees/python/installation_python.doctree
diff --git a/_build/doctrees/python/prerequisites_python.doctree b/_build/doctrees/python/prerequisites_python.doctree
diff --git a/_build/doctrees/python/sample/absorption_python_sample.doctree b/_build/doctrees/python/sample/absorption_python_sample.doctree
diff --git a/_build/doctrees/python/sample/biconditional_elimination_1_python_sample.doctree b/_build/doctrees/python/sample/biconditional_elimination_1_python_sample.doctree
diff --git a/_build/doctrees/python/sample/biconditional_elimination_2_python_sample.doctree b/_build/doctrees/python/sample/biconditional_elimination_2_python_sample.doctree
diff --git a/_build/doctrees/python/sample/biconditional_introduction_python_sample.doctree b/_build/doctrees/python/sample/biconditional_introduction_python_sample.doctree
diff --git a/_build/doctrees/python/sample/conjunction_elimination_1_python_sample.doctree b/_build/doctrees/python/sample/conjunction_elimination_1_python_sample.doctree
diff --git a/_build/doctrees/python/sample/conjunction_elimination_2_python_sample.doctree b/_build/doctrees/python/sample/conjunction_elimination_2_python_sample.doctree
diff --git a/_build/doctrees/python/sample/conjunction_introduction_python_sample.doctree b/_build/doctrees/python/sample/conjunction_introduction_python_sample.doctree
diff --git a/_build/doctrees/python/sample/disjunction_introduction_1_python_sample.doctree b/_build/doctrees/python/sample/disjunction_introduction_1_python_sample.doctree
diff --git a/_build/doctrees/python/sample/disjunction_introduction_2_python_sample.doctree b/_build/doctrees/python/sample/disjunction_introduction_2_python_sample.doctree
diff --git a/_build/doctrees/python/sample/double_negation_elimination_python_sample.doctree b/_build/doctrees/python/sample/double_negation_elimination_python_sample.doctree
diff --git a/_build/doctrees/python/sample/double_negation_introduction_python_sample.doctree b/_build/doctrees/python/sample/double_negation_introduction_python_sample.doctree
diff --git a/_build/doctrees/python/sample/equal_terms_substitution_python_sample.doctree b/_build/doctrees/python/sample/equal_terms_substitution_python_sample.doctree
diff --git a/_build/doctrees/python/sample/equality_commutativity_python_sample.doctree b/_build/doctrees/python/sample/equality_commutativity_python_sample.doctree
diff --git a/_build/doctrees/python/sample/inconsistency_introduction_1_python_sample.doctree b/_build/doctrees/python/sample/inconsistency_introduction_1_python_sample.doctree
diff --git a/_build/doctrees/python/sample/inconsistency_introduction_2_python_sample.doctree b/_build/doctrees/python/sample/inconsistency_introduction_2_python_sample.doctree
diff --git a/_build/doctrees/python/sample/inconsistency_introduction_3_python_sample.doctree b/_build/doctrees/python/sample/inconsistency_introduction_3_python_sample.doctree
diff --git a/_build/doctrees/python/sample/modus_ponens_python_sample.doctree b/_build/doctrees/python/sample/modus_ponens_python_sample.doctree
diff --git a/_build/doctrees/python/sample/proof_by_contradiction_1_python_sample.doctree b/_build/doctrees/python/sample/proof_by_contradiction_1_python_sample.doctree
diff --git a/_build/doctrees/python/sample/proof_by_contradiction_2_python_sample.doctree b/_build/doctrees/python/sample/proof_by_contradiction_2_python_sample.doctree
diff --git a/_build/doctrees/python/sample/proof_by_refutation_1_python_sample.doctree b/_build/doctrees/python/sample/proof_by_refutation_1_python_sample.doctree
diff --git a/_build/doctrees/python/sample/proof_by_refutation_2_python_sample.doctree b/_build/doctrees/python/sample/proof_by_refutation_2_python_sample.doctree
diff --git a/_build/doctrees/python/sample/python_sample_index.doctree b/_build/doctrees/python/sample/python_sample_index.doctree
diff --git a/_build/doctrees/python/sample/variable_substitution_python_sample.doctree b/_build/doctrees/python/sample/variable_substitution_python_sample.doctree
diff --git a/_build/doctrees/python/source_code_repository_python.doctree b/_build/doctrees/python/source_code_repository_python.doctree
diff --git a/branding/github-repository-social-media-preview.png b/branding/github-repository-social-media-preview.png
diff --git a/branding/github-repository-social-media-preview.svg b/branding/github-repository-social-media-preview.svg
diff --git a/continuous_integration/scripts/release_patch.ps1 b/continuous_integration/scripts/release_patch.ps1
@@ -29,7 +29,7 @@ Write-Output "Script: $( $script ). Step: $( $current_step ) / $( $total_step ).
 & $PSScriptRoot\build_package.ps1
 
 $current_step = 4
-$command = "release_package.ps1"
+$command = "distribute_package_to_pypi.ps1"
 Write-Output "Script: $( $script ). Step: $( $current_step ) / $( $total_step ). $( $command )"
-& $PSScriptRoot\release_package.ps1
+& $PSScriptRoot\distribute_package_to_pypi.ps1
 
diff --git a/dist/punctilious-1.0.9-py3-none-any.whl b/dist/punctilious-1.0.9-py3-none-any.whl
diff --git a/dist/punctilious-1.0.9.tar.gz b/dist/punctilious-1.0.9.tar.gz
diff --git a/docs/build/.buildinfo b/docs/build/.buildinfo
@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: bc5fc4b808bdc74de5382c916c2be562
+config: 6c73ab850cba538aa85362694c74af3e
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/docs/build/_static/basic.css b/docs/build/_static/basic.css
@@ -237,6 +237,10 @@ a.headerlink {
     visibility: hidden;
 }
 
+a:visited {
+    color: #551A8B;
+}
+
 h1:hover > a.headerlink,
 h2:hover > a.headerlink,
 h3:hover > a.headerlink,

diff --git a/docs/build/_static/documentation_options.js b/docs/build/_static/documentation_options.js
@@ -1,6 +1,5 @@
-var DOCUMENTATION_OPTIONS = {
-    URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'),
-    VERSION: '1.0.8',
+const DOCUMENTATION_OPTIONS = {
+    VERSION: '1.0.9',
     LANGUAGE: 'en',
     COLLAPSE_INDEX: false,
     BUILDER: 'html',

diff --git a/docs/build/_static/pygments.css b/docs/build/_static/pygments.css
@@ -17,6 +17,7 @@ span.linenos.special { color: #000000; background-color: #ffffc0; padding-left:
 .highlight .cs { color: #3D7B7B; font-style: italic } /* Comment.Special */
 .highlight .gd { color: #A00000 } /* Generic.Deleted */
 .highlight .ge { font-style: italic } /* Generic.Emph */
+.highlight .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */
 .highlight .gr { color: #E40000 } /* Generic.Error */
 .highlight .gh { color: #000080; font-weight: bold } /* Generic.Heading */
 .highlight .gi { color: #008400 } /* Generic.Inserted */

diff --git a/docs/build/_static/searchtools.js b/docs/build/_static/searchtools.js
@@ -57,12 +57,12 @@ const _removeChildren = (element) => {
 const _escapeRegExp = (string) =>
   string.replace(/[.*+\-?^${}()|[\]\\]/g, "\\$&"); // $& means the whole matched string
 
-const _displayItem = (item, searchTerms) => {
+const _displayItem = (item, searchTerms, highlightTerms) => {
   const docBuilder = DOCUMENTATION_OPTIONS.BUILDER;
-  const docUrlRoot = DOCUMENTATION_OPTIONS.URL_ROOT;
   const docFileSuffix = DOCUMENTATION_OPTIONS.FILE_SUFFIX;
   const docLinkSuffix = DOCUMENTATION_OPTIONS.LINK_SUFFIX;
   const showSearchSummary = DOCUMENTATION_OPTIONS.SHOW_SEARCH_SUMMARY;
+  const contentRoot = document.documentElement.dataset.content_root;
 
   const [docName, title, anchor, descr, score, _filename] = item;
 
@@ -75,20 +75,24 @@ const _displayItem = (item, searchTerms) => {
     if (dirname.match(/\/index\/$/))
       dirname = dirname.substring(0, dirname.length - 6);
     else if (dirname === "index/") dirname = "";
-    requestUrl = docUrlRoot + dirname;
+    requestUrl = contentRoot + dirname;
     linkUrl = requestUrl;
   } else {
     // normal html builders
-    requestUrl = docUrlRoot + docName + docFileSuffix;
+    requestUrl = contentRoot + docName + docFileSuffix;
     linkUrl = docName + docLinkSuffix;
   }
   let linkEl = listItem.appendChild(document.createElement("a"));
   linkEl.href = linkUrl + anchor;
   linkEl.dataset.score = score;
   linkEl.innerHTML = title;
-  if (descr)
+  if (descr) {
     listItem.appendChild(document.createElement("span")).innerHTML =
       " (" + descr + ")";
+    // highlight search terms in the description
+    if (SPHINX_HIGHLIGHT_ENABLED)  // set in sphinx_highlight.js
+      highlightTerms.forEach((term) => _highlightText(listItem, term, "highlighted"));
+  }
   else if (showSearchSummary)
     fetch(requestUrl)
       .then((responseData) => responseData.text())
@@ -97,6 +101,9 @@ const _displayItem = (item, searchTerms) => {
           listItem.appendChild(
             Search.makeSearchSummary(data, searchTerms)
           );
+        // highlight search terms in the summary
+        if (SPHINX_HIGHLIGHT_ENABLED)  // set in sphinx_highlight.js
+          highlightTerms.forEach((term) => _highlightText(listItem, term, "highlighted"));
       });
   Search.output.appendChild(listItem);
 };
@@ -115,14 +122,15 @@ const _finishSearch = (resultCount) => {
 const _displayNextItem = (
   results,
   resultCount,
-  searchTerms
+  searchTerms,
+  highlightTerms,
 ) => {
   // results left, load the summary and display it
   // this is intended to be dynamic (don't sub resultsCount)
   if (results.length) {
-    _displayItem(results.pop(), searchTerms);
+    _displayItem(results.pop(), searchTerms, highlightTerms);
     setTimeout(
-      () => _displayNextItem(results, resultCount, searchTerms),
+      () => _displayNextItem(results, resultCount, searchTerms, highlightTerms),
       5
     );
   }
@@ -360,7 +368,7 @@ const Search = {
     // console.info("search results:", Search.lastresults);
 
     // print the results
-    _displayNextItem(results, results.length, searchTerms);
+    _displayNextItem(results, results.length, searchTerms, highlightTerms);
   },
 
   /**

diff --git a/docs/build/_static/sphinx_highlight.js b/docs/build/_static/sphinx_highlight.js
@@ -29,14 +29,19 @@ const _highlight = (node, addItems, text, className) => {
       }
 
       span.appendChild(document.createTextNode(val.substr(pos, text.length)));
+      const rest = document.createTextNode(val.substr(pos + text.length));
       parent.insertBefore(
         span,
         parent.insertBefore(
-          document.createTextNode(val.substr(pos + text.length)),
+          rest,
           node.nextSibling
         )
       );
       node.nodeValue = val.substr(0, pos);
+      /* There may be more occurrences of search term in this node. So call this
+       * function recursively on the remaining fragment.
+       */
+      _highlight(rest, addItems, text, className);
 
       if (isInSVG) {
         const rect = document.createElementNS(
@@ -140,5 +145,10 @@ const SphinxHighlight = {
   },
 };
 
-_ready(SphinxHighlight.highlightSearchWords);
-_ready(SphinxHighlight.initEscapeListener);
+_ready(() => {
+  /* Do not call highlightSearchWords() when we are on the search page.
+   * It will highlight words from the *previous* search query.
+   */
+  if (typeof Search === "undefined") SphinxHighlight.highlightSearchWords();
+  SphinxHighlight.initEscapeListener();
+});
diff --git a/docs/build/_tags/absorption.html b/docs/build/_tags/absorption.html
@@ -2,14 +2,14 @@
 <html class="writer-html5" lang="en">
 <head>
     <meta charset="utf-8"/>
-    <meta name="viewport" content="width=device-width, initial-scale=1"/>
+    <meta name="generator" content="Docutils 0.18.1: http://docutils.sourceforge.net/"/>
     <link href="../_static/punctilious-logo-compact-light.svg" rel="icon" type="image/svg+xml">
     <link href="../_static/punctilious-logo-compact-light-16x16-white.png" sizes="16x16" rel="icon" type="image/png">
     <link href="../_static/punctilious-logo-compact-light-32x32-white.png" sizes="32x32" rel="icon" type="image/png">
     <link rel="apple-touch-icon" href="../_static/punctilious-logo-compact-light-180x180-white.png" sizes="180x180"
           type="image/png">
     <meta name="viewport" content="width=device-width, initial-scale=1.0"/>
-    <title>My tags: absorption &mdash; punctilious 1.0.8 documentation</title>
+    <title>My tags: absorption &mdash; punctilious 1.0.9 documentation</title>
     <link rel="stylesheet" href="../_static/pygments.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/css/theme.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/graphviz.css" type="text/css"/>
@@ -23,16 +23,16 @@
 
     <script src="../_static/jquery.js?v=5d32c60e"></script>
     <script src="../_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
-    <script data-url_root="../" id="documentation_options"
-            src="../_static/documentation_options.js?v=8cbfd27f"></script>
+    <script src="../_static/documentation_options.js?v=0abd802e"></script>
     <script src="../_static/doctools.js?v=888ff710"></script>
-    <script src="../_static/sphinx_highlight.js?v=4825356b"></script>
+    <script src="../_static/sphinx_highlight.js?v=dc90522c"></script>
     <script>let toggleHintShow = 'Click to show';</script>
     <script>let toggleHintHide = 'Click to hide';</script>
     <script>let toggleOpenOnPrint = 'true';</script>
     <script src="../_static/togglebutton.js?v=4a39c7ea"></script>
     <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/design-tabs.js?v=36754332"></script>
+    <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/js/theme.js"></script>
     <link rel="index" title="Index" href="../genindex.html"/>
     <link rel="search" title="Search" href="../search.html"/>
@@ -92,7 +92,7 @@
 
                         <section id="my-tags-absorption">
                             <h1>My tags: absorption<a class="headerlink" href="#my-tags-absorption"
-                                                      title="Permalink to this heading"></a></h1>
+                                                      title="Link to this heading"></a></h1>
                             <div class="toctree-wrapper compound">
                                 <p class="caption" role="heading"><span class="caption-text">With this tag</span></p>
                                 <ul>

diff --git a/docs/build/_tags/biconditional-elimination-1.html b/docs/build/_tags/biconditional-elimination-1.html
@@ -2,14 +2,14 @@
 <html class="writer-html5" lang="en">
 <head>
     <meta charset="utf-8"/>
-    <meta name="viewport" content="width=device-width, initial-scale=1"/>
+    <meta name="generator" content="Docutils 0.18.1: http://docutils.sourceforge.net/"/>
     <link href="../_static/punctilious-logo-compact-light.svg" rel="icon" type="image/svg+xml">
     <link href="../_static/punctilious-logo-compact-light-16x16-white.png" sizes="16x16" rel="icon" type="image/png">
     <link href="../_static/punctilious-logo-compact-light-32x32-white.png" sizes="32x32" rel="icon" type="image/png">
     <link rel="apple-touch-icon" href="../_static/punctilious-logo-compact-light-180x180-white.png" sizes="180x180"
           type="image/png">
     <meta name="viewport" content="width=device-width, initial-scale=1.0"/>
-    <title>My tags: biconditional-elimination-1 &mdash; punctilious 1.0.8 documentation</title>
+    <title>My tags: biconditional-elimination-1 &mdash; punctilious 1.0.9 documentation</title>
     <link rel="stylesheet" href="../_static/pygments.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/css/theme.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/graphviz.css" type="text/css"/>
@@ -23,16 +23,16 @@
 
     <script src="../_static/jquery.js?v=5d32c60e"></script>
     <script src="../_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
-    <script data-url_root="../" id="documentation_options"
-            src="../_static/documentation_options.js?v=8cbfd27f"></script>
+    <script src="../_static/documentation_options.js?v=0abd802e"></script>
     <script src="../_static/doctools.js?v=888ff710"></script>
-    <script src="../_static/sphinx_highlight.js?v=4825356b"></script>
+    <script src="../_static/sphinx_highlight.js?v=dc90522c"></script>
     <script>let toggleHintShow = 'Click to show';</script>
     <script>let toggleHintHide = 'Click to hide';</script>
     <script>let toggleOpenOnPrint = 'true';</script>
     <script src="../_static/togglebutton.js?v=4a39c7ea"></script>
     <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/design-tabs.js?v=36754332"></script>
+    <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/js/theme.js"></script>
     <link rel="index" title="Index" href="../genindex.html"/>
     <link rel="search" title="Search" href="../search.html"/>
@@ -94,7 +94,7 @@
                         <section id="my-tags-biconditional-elimination-1">
                             <h1>My tags: biconditional-elimination-1<a class="headerlink"
                                                                        href="#my-tags-biconditional-elimination-1"
-                                                                       title="Permalink to this heading"></a></h1>
+                                                                       title="Link to this heading"></a></h1>
                             <div class="toctree-wrapper compound">
                                 <p class="caption" role="heading"><span class="caption-text">With this tag</span></p>
                                 <ul>

diff --git a/docs/build/_tags/biconditional-elimination-2.html b/docs/build/_tags/biconditional-elimination-2.html
@@ -2,14 +2,14 @@
 <html class="writer-html5" lang="en">
 <head>
     <meta charset="utf-8"/>
-    <meta name="viewport" content="width=device-width, initial-scale=1"/>
+    <meta name="generator" content="Docutils 0.18.1: http://docutils.sourceforge.net/"/>
     <link href="../_static/punctilious-logo-compact-light.svg" rel="icon" type="image/svg+xml">
     <link href="../_static/punctilious-logo-compact-light-16x16-white.png" sizes="16x16" rel="icon" type="image/png">
     <link href="../_static/punctilious-logo-compact-light-32x32-white.png" sizes="32x32" rel="icon" type="image/png">
     <link rel="apple-touch-icon" href="../_static/punctilious-logo-compact-light-180x180-white.png" sizes="180x180"
           type="image/png">
     <meta name="viewport" content="width=device-width, initial-scale=1.0"/>
-    <title>My tags: biconditional-elimination-2 &mdash; punctilious 1.0.8 documentation</title>
+    <title>My tags: biconditional-elimination-2 &mdash; punctilious 1.0.9 documentation</title>
     <link rel="stylesheet" href="../_static/pygments.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/css/theme.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/graphviz.css" type="text/css"/>
@@ -23,16 +23,16 @@
 
     <script src="../_static/jquery.js?v=5d32c60e"></script>
     <script src="../_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
-    <script data-url_root="../" id="documentation_options"
-            src="../_static/documentation_options.js?v=8cbfd27f"></script>
+    <script src="../_static/documentation_options.js?v=0abd802e"></script>
     <script src="../_static/doctools.js?v=888ff710"></script>
-    <script src="../_static/sphinx_highlight.js?v=4825356b"></script>
+    <script src="../_static/sphinx_highlight.js?v=dc90522c"></script>
     <script>let toggleHintShow = 'Click to show';</script>
     <script>let toggleHintHide = 'Click to hide';</script>
     <script>let toggleOpenOnPrint = 'true';</script>
     <script src="../_static/togglebutton.js?v=4a39c7ea"></script>
     <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/design-tabs.js?v=36754332"></script>
+    <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/js/theme.js"></script>
     <link rel="index" title="Index" href="../genindex.html"/>
     <link rel="search" title="Search" href="../search.html"/>
@@ -94,7 +94,7 @@
                         <section id="my-tags-biconditional-elimination-2">
                             <h1>My tags: biconditional-elimination-2<a class="headerlink"
                                                                        href="#my-tags-biconditional-elimination-2"
-                                                                       title="Permalink to this heading"></a></h1>
+                                                                       title="Link to this heading"></a></h1>
                             <div class="toctree-wrapper compound">
                                 <p class="caption" role="heading"><span class="caption-text">With this tag</span></p>
                                 <ul>

diff --git a/docs/build/_tags/biconditional-introduction.html b/docs/build/_tags/biconditional-introduction.html
@@ -2,14 +2,14 @@
 <html class="writer-html5" lang="en">
 <head>
     <meta charset="utf-8"/>
-    <meta name="viewport" content="width=device-width, initial-scale=1"/>
+    <meta name="generator" content="Docutils 0.18.1: http://docutils.sourceforge.net/"/>
     <link href="../_static/punctilious-logo-compact-light.svg" rel="icon" type="image/svg+xml">
     <link href="../_static/punctilious-logo-compact-light-16x16-white.png" sizes="16x16" rel="icon" type="image/png">
     <link href="../_static/punctilious-logo-compact-light-32x32-white.png" sizes="32x32" rel="icon" type="image/png">
     <link rel="apple-touch-icon" href="../_static/punctilious-logo-compact-light-180x180-white.png" sizes="180x180"
           type="image/png">
     <meta name="viewport" content="width=device-width, initial-scale=1.0"/>
-    <title>My tags: biconditional-introduction &mdash; punctilious 1.0.8 documentation</title>
+    <title>My tags: biconditional-introduction &mdash; punctilious 1.0.9 documentation</title>
     <link rel="stylesheet" href="../_static/pygments.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/css/theme.css" type="text/css"/>
     <link rel="stylesheet" href="../_static/graphviz.css" type="text/css"/>
@@ -23,16 +23,16 @@
 
     <script src="../_static/jquery.js?v=5d32c60e"></script>
     <script src="../_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
-    <script data-url_root="../" id="documentation_options"
-            src="../_static/documentation_options.js?v=8cbfd27f"></script>
+    <script src="../_static/documentation_options.js?v=0abd802e"></script>
     <script src="../_static/doctools.js?v=888ff710"></script>
-    <script src="../_static/sphinx_highlight.js?v=4825356b"></script>
+    <script src="../_static/sphinx_highlight.js?v=dc90522c"></script>
     <script>let toggleHintShow = 'Click to show';</script>
     <script>let toggleHintHide = 'Click to hide';</script>
     <script>let toggleOpenOnPrint = 'true';</script>
     <script src="../_static/togglebutton.js?v=4a39c7ea"></script>
     <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/design-tabs.js?v=36754332"></script>
+    <script>var togglebuttonSelector = '.toggle, .admonition.dropdown';</script>
     <script src="../_static/js/theme.js"></script>
     <link rel="index" title="Index" href="../genindex.html"/>
     <link rel="search" title="Search" href="../search.html"/>
@@ -94,7 +94,7 @@
                         <section id="my-tags-biconditional-introduction">
                             <h1>My tags: biconditional-introduction<a class="headerlink"
                                                                       href="#my-tags-biconditional-introduction"
-                                                                      title="Permalink to this heading"></a></h1>
+                                                                      title="Link to this heading"></a></h1>
                             <div class="toctree-wrapper compound">
                                 <p class="caption" role="heading"><span class="caption-text">With this tag</span></p>
                                 <ul>