From 7e2224859e0f3975db156805c0a15f285e0caec8 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Mon, 22 Jun 2020 17:42:40 +0200 Subject: [PATCH] mmm --- .ci/Jenkinsfile | 0 .ci/isabelle4isadof/Dockerfile | 0 .config | 0 .gitattributes | 0 .gitignore | 0 CHANGELOG.md | 0 CITATION | 0 LICENSE | 0 README.md | 0 ROOTS | 0 examples/CENELEC_50128/ROOTS | 0 examples/CENELEC_50128/mini_odo/ROOT | 0 .../document/figures/df-numerics-encshaft.png | Bin .../mini_odo/document/figures/odometer.jpeg | Bin .../mini_odo/document/figures/three-phase-odo.pdf | Bin .../mini_odo/document/figures/wheel-df.png | Bin examples/CENELEC_50128/mini_odo/document/isadof.cfg | 0 .../CENELEC_50128/mini_odo/document/lstisadof.sty | 0 .../CENELEC_50128/mini_odo/document/preamble.tex | 0 examples/CENELEC_50128/mini_odo/document/root.bib | 0 examples/CENELEC_50128/mini_odo/document/root.mst | 0 examples/CENELEC_50128/mini_odo/mini_odo.thy | 0 examples/README.md | 0 examples/ROOTS | 0 examples/math_exam/MathExam/MathExam.thy | 0 examples/math_exam/MathExam/ROOT | 0 .../MathExam/document/figures/Polynomialdeg5.png | Bin examples/math_exam/MathExam/document/isadof.cfg | 0 examples/math_exam/MathExam/document/preamble.tex | 0 examples/math_exam/ROOTS | 0 .../IsaDofApplications.thy | 0 .../2018-cicm-isabelle_dof-applications/ROOT | 0 .../document/figures/Dogfood-II-bgnd1.png | Bin .../figures/Dogfood-III-bgnd-text_section.png | Bin .../document/figures/Dogfood-IV-jumpInDocCLass.png | Bin .../document/figures/Dogfood-Intro.png | Bin .../document/figures/Dogfood-V-attribute.png | Bin .../document/figures/Dogfood-figures.png | Bin .../document/figures/InteractiveMathSheet.png | Bin .../document/figures/antiquotations-PIDE.png | Bin .../document/figures/isabelle-architecture.pdf | Bin .../document/figures/isabelle-architecture.svg | 0 .../document/figures/srac-as-es-application.png | Bin .../document/figures/srac-definition.png | Bin .../document/isadof.cfg | 0 .../document/lstisadof.sty | 0 .../document/preamble.tex | 0 .../document/root.bib | 0 examples/scholarly_paper/ROOTS | 0 .../Isabelle_DOF-Manual/00_Frontmatter.thy | 0 .../Isabelle_DOF-Manual/01_Introduction.thy | 0 .../Isabelle_DOF-Manual/02_Background.thy | 0 .../Isabelle_DOF-Manual/03_GuidedTour.thy | 0 .../Isabelle_DOF-Manual/04_RefMan.thy | 0 .../Isabelle_DOF-Manual/05_Implementation.thy | 0 .../Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy | 0 examples/technical_report/Isabelle_DOF-Manual/ROOT | 0 .../document/figures/Dogfood-II-bgnd1.png | Bin .../figures/Dogfood-III-bgnd-text_section.png | Bin .../document/figures/Dogfood-IV-jumpInDocCLass.png | Bin .../document/figures/Dogfood-Intro.png | Bin .../document/figures/Dogfood-V-attribute.png | Bin .../document/figures/Dogfood-figures.png | Bin .../document/figures/Isabelle_DOF-logo.pdf | Bin .../document/figures/antiquotations-PIDE.png | Bin .../document/figures/cicm2018-combined.png | Bin .../document/figures/cicm2018-dof.png | Bin .../document/figures/cicm2018-pdf.png | Bin .../document/figures/document-hierarchy.pdf | Bin .../document/figures/document-hierarchy.svg | 0 .../document/figures/isabelle-architecture.pdf | Bin .../document/figures/isabelle-architecture.svg | 0 .../Isabelle_DOF-Manual/document/figures/isadof.png | Bin .../document/figures/srac-as-es-application.png | Bin .../document/figures/srac-definition.png | Bin .../Isabelle_DOF-Manual/document/isadof.cfg | 0 .../document/lstisadof-manual.sty | 0 .../Isabelle_DOF-Manual/document/preamble.tex | 0 .../Isabelle_DOF-Manual/document/root.bib | 0 .../Isabelle_DOF-Manual/document/root.mst | 0 examples/technical_report/ROOTS | 0 .../technical_report/TR_my_commented_isabelle/ROOT | 0 .../TR_MyCommentedIsabelle.thy | 0 .../document/figures/document-model.pdf | Bin .../document/figures/isabelle-architecture.pdf | Bin .../document/figures/markup-demo.png | Bin .../document/figures/pure-inferences-I.pdf | Bin .../document/figures/pure-inferences-II.pdf | Bin .../document/figures/text-element.pdf | Bin .../TR_my_commented_isabelle/document/isadof.cfg | 0 .../TR_my_commented_isabelle/document/preamble.tex | 0 .../TR_my_commented_isabelle/document/prooftree.sty | 0 .../TR_my_commented_isabelle/document/root.bib | 0 src/DOF/Assert.thy | 0 src/DOF/AssertLong.thy | 0 src/DOF/Isa_COL.thy | 0 src/DOF/Isa_DOF.thy | 0 src/DOF/RegExpInterface.thy | 0 src/DOF/latex/DOF-COL.sty | 0 src/DOF/latex/DOF-core.sty | 0 src/ROOT | 0 src/ROOTS | 0 src/SI/Groups_mult.thy | 0 src/SI/ISQ.thy | 0 src/SI/ISQ_Algebra.thy | 0 src/SI/ISQ_Dimensions.thy | 0 src/SI/ISQ_Proof.thy | 0 src/SI/ISQ_Quantities.thy | 0 src/SI/ROOT | 0 src/SI/SI.thy | 0 src/SI/SIOld.thy | 0 src/SI/SI_Accepted.thy | 0 src/SI/SI_Astronomical.thy | 0 src/SI/SI_Constants.thy | 0 src/SI/SI_Derived.thy | 0 src/SI/SI_Imperial.thy | 0 src/SI/SI_Prefix.thy | 0 src/SI/SI_Units.thy | 0 src/SI/document/adb-long.bib | 0 src/SI/document/root.bib | 0 src/SI/document/root.tex | 0 src/document-templates/root-eptcs-UNSUPPORTED.tex | 0 .../root-lipics-v2019-UNSUPPORTED.tex | 0 src/document-templates/root-lncs.tex | 0 src/document-templates/root-scrartcl.tex | 0 src/document-templates/root-scrreprt-modern.tex | 0 src/document-templates/root-scrreprt.tex | 0 src/ontologies/CENELEC_50128/CENELEC_50128.thy | 0 src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty | 0 src/ontologies/Conceptual/Conceptual.thy | 0 src/ontologies/math_exam/DOF-math_exam.sty | 0 src/ontologies/math_exam/Nmath_exam.thy | 0 src/ontologies/math_exam/math_exam.thy | 0 src/ontologies/math_paper/math_paper.thy | 0 src/ontologies/ontologies.thy | 0 .../scholarly_paper/DOF-scholarly_paper.sty | 0 src/ontologies/scholarly_paper/scholarly_paper.thy | 0 src/ontologies/small_math/small_math.thy | 0 .../technical_report/DOF-technical_report.sty | 0 .../technical_report/technical_report.thy | 0 src/patches/thy_output.Isabelle2020.ML | 0 src/patches/thy_output.ML | 0 src/tests/AssnsLemmaThmEtc.thy | 0 src/tests/Attributes.thy | 0 src/tests/Concept_Example.thy | 0 src/tests/Concept_ExampleInvariant.thy | 0 src/tests/InnerSyntaxAntiquotations.thy | 0 src/tests/ROOT | 0 src/tests/figures/A.png | Bin src/tests/figures/AnB.odp | Bin src/tests/figures/B.png | Bin 151 files changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 .ci/Jenkinsfile mode change 100644 => 100755 .ci/isabelle4isadof/Dockerfile mode change 100644 => 100755 .config mode change 100644 => 100755 .gitattributes mode change 100644 => 100755 .gitignore mode change 100644 => 100755 CHANGELOG.md mode change 100644 => 100755 CITATION mode change 100644 => 100755 LICENSE mode change 100644 => 100755 README.md mode change 100644 => 100755 ROOTS mode change 100644 => 100755 examples/CENELEC_50128/ROOTS mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/ROOT mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/isadof.cfg mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/lstisadof.sty mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/preamble.tex mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/root.bib mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/document/root.mst mode change 100644 => 100755 examples/CENELEC_50128/mini_odo/mini_odo.thy mode change 100644 => 100755 examples/README.md mode change 100644 => 100755 examples/ROOTS mode change 100644 => 100755 examples/math_exam/MathExam/MathExam.thy mode change 100644 => 100755 examples/math_exam/MathExam/ROOT mode change 100644 => 100755 examples/math_exam/MathExam/document/figures/Polynomialdeg5.png mode change 100644 => 100755 examples/math_exam/MathExam/document/isadof.cfg mode change 100644 => 100755 examples/math_exam/MathExam/document/preamble.tex mode change 100644 => 100755 examples/math_exam/ROOTS mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex mode change 100644 => 100755 examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib mode change 100644 => 100755 examples/scholarly_paper/ROOTS mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/02_Background.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/ROOT mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/root.bib mode change 100644 => 100755 examples/technical_report/Isabelle_DOF-Manual/document/root.mst mode change 100644 => 100755 examples/technical_report/ROOTS mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/ROOT mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/preamble.tex mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty mode change 100644 => 100755 examples/technical_report/TR_my_commented_isabelle/document/root.bib mode change 100644 => 100755 src/DOF/Assert.thy mode change 100644 => 100755 src/DOF/AssertLong.thy mode change 100644 => 100755 src/DOF/Isa_COL.thy mode change 100644 => 100755 src/DOF/Isa_DOF.thy mode change 100644 => 100755 src/DOF/RegExpInterface.thy mode change 100644 => 100755 src/DOF/latex/DOF-COL.sty mode change 100644 => 100755 src/DOF/latex/DOF-core.sty mode change 100644 => 100755 src/ROOT mode change 100644 => 100755 src/ROOTS mode change 100644 => 100755 src/SI/Groups_mult.thy mode change 100644 => 100755 src/SI/ISQ.thy mode change 100644 => 100755 src/SI/ISQ_Algebra.thy mode change 100644 => 100755 src/SI/ISQ_Dimensions.thy mode change 100644 => 100755 src/SI/ISQ_Proof.thy mode change 100644 => 100755 src/SI/ISQ_Quantities.thy mode change 100644 => 100755 src/SI/ROOT mode change 100644 => 100755 src/SI/SI.thy mode change 100644 => 100755 src/SI/SIOld.thy mode change 100644 => 100755 src/SI/SI_Accepted.thy mode change 100644 => 100755 src/SI/SI_Astronomical.thy mode change 100644 => 100755 src/SI/SI_Constants.thy mode change 100644 => 100755 src/SI/SI_Derived.thy mode change 100644 => 100755 src/SI/SI_Imperial.thy mode change 100644 => 100755 src/SI/SI_Prefix.thy mode change 100644 => 100755 src/SI/SI_Units.thy mode change 100644 => 100755 src/SI/document/adb-long.bib mode change 100644 => 100755 src/SI/document/root.bib mode change 100644 => 100755 src/SI/document/root.tex mode change 100644 => 100755 src/document-templates/root-eptcs-UNSUPPORTED.tex mode change 100644 => 100755 src/document-templates/root-lipics-v2019-UNSUPPORTED.tex mode change 100644 => 100755 src/document-templates/root-lncs.tex mode change 100644 => 100755 src/document-templates/root-scrartcl.tex mode change 100644 => 100755 src/document-templates/root-scrreprt-modern.tex mode change 100644 => 100755 src/document-templates/root-scrreprt.tex mode change 100644 => 100755 src/ontologies/CENELEC_50128/CENELEC_50128.thy mode change 100644 => 100755 src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty mode change 100644 => 100755 src/ontologies/Conceptual/Conceptual.thy mode change 100644 => 100755 src/ontologies/math_exam/DOF-math_exam.sty mode change 100644 => 100755 src/ontologies/math_exam/Nmath_exam.thy mode change 100644 => 100755 src/ontologies/math_exam/math_exam.thy mode change 100644 => 100755 src/ontologies/math_paper/math_paper.thy mode change 100644 => 100755 src/ontologies/ontologies.thy mode change 100644 => 100755 src/ontologies/scholarly_paper/DOF-scholarly_paper.sty mode change 100644 => 100755 src/ontologies/scholarly_paper/scholarly_paper.thy mode change 100644 => 100755 src/ontologies/small_math/small_math.thy mode change 100644 => 100755 src/ontologies/technical_report/DOF-technical_report.sty mode change 100644 => 100755 src/ontologies/technical_report/technical_report.thy mode change 100644 => 100755 src/patches/thy_output.Isabelle2020.ML mode change 100644 => 100755 src/patches/thy_output.ML mode change 100644 => 100755 src/tests/AssnsLemmaThmEtc.thy mode change 100644 => 100755 src/tests/Attributes.thy mode change 100644 => 100755 src/tests/Concept_Example.thy mode change 100644 => 100755 src/tests/Concept_ExampleInvariant.thy mode change 100644 => 100755 src/tests/InnerSyntaxAntiquotations.thy mode change 100644 => 100755 src/tests/ROOT mode change 100644 => 100755 src/tests/figures/A.png mode change 100644 => 100755 src/tests/figures/AnB.odp mode change 100644 => 100755 src/tests/figures/B.png diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile old mode 100644 new mode 100755 diff --git a/.ci/isabelle4isadof/Dockerfile b/.ci/isabelle4isadof/Dockerfile old mode 100644 new mode 100755 diff --git a/.config b/.config old mode 100644 new mode 100755 diff --git a/.gitattributes b/.gitattributes old mode 100644 new mode 100755 diff --git a/.gitignore b/.gitignore old mode 100644 new mode 100755 diff --git a/CHANGELOG.md b/CHANGELOG.md old mode 100644 new mode 100755 diff --git a/CITATION b/CITATION old mode 100644 new mode 100755 diff --git a/LICENSE b/LICENSE old mode 100644 new mode 100755 diff --git a/README.md b/README.md old mode 100644 new mode 100755 diff --git a/ROOTS b/ROOTS old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/ROOTS b/examples/CENELEC_50128/ROOTS old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png b/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg b/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf b/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png b/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/isadof.cfg b/examples/CENELEC_50128/mini_odo/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/lstisadof.sty b/examples/CENELEC_50128/mini_odo/document/lstisadof.sty old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/preamble.tex b/examples/CENELEC_50128/mini_odo/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/root.bib b/examples/CENELEC_50128/mini_odo/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/root.mst b/examples/CENELEC_50128/mini_odo/document/root.mst old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy old mode 100644 new mode 100755 diff --git a/examples/README.md b/examples/README.md old mode 100644 new mode 100755 diff --git a/examples/ROOTS b/examples/ROOTS old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png b/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/isadof.cfg b/examples/math_exam/MathExam/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/preamble.tex b/examples/math_exam/MathExam/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/math_exam/ROOTS b/examples/math_exam/ROOTS old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/ROOTS b/examples/scholarly_paper/ROOTS old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg b/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.mst b/examples/technical_report/Isabelle_DOF-Manual/document/root.mst old mode 100644 new mode 100755 diff --git a/examples/technical_report/ROOTS b/examples/technical_report/ROOTS old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg b/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex b/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty b/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.bib b/examples/technical_report/TR_my_commented_isabelle/document/root.bib old mode 100644 new mode 100755 diff --git a/src/DOF/Assert.thy b/src/DOF/Assert.thy old mode 100644 new mode 100755 diff --git a/src/DOF/AssertLong.thy b/src/DOF/AssertLong.thy old mode 100644 new mode 100755 diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy old mode 100644 new mode 100755 diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy old mode 100644 new mode 100755 diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy old mode 100644 new mode 100755 diff --git a/src/DOF/latex/DOF-COL.sty b/src/DOF/latex/DOF-COL.sty old mode 100644 new mode 100755 diff --git a/src/DOF/latex/DOF-core.sty b/src/DOF/latex/DOF-core.sty old mode 100644 new mode 100755 diff --git a/src/ROOT b/src/ROOT old mode 100644 new mode 100755 diff --git a/src/ROOTS b/src/ROOTS old mode 100644 new mode 100755 diff --git a/src/SI/Groups_mult.thy b/src/SI/Groups_mult.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ.thy b/src/SI/ISQ.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Algebra.thy b/src/SI/ISQ_Algebra.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Proof.thy b/src/SI/ISQ_Proof.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy old mode 100644 new mode 100755 diff --git a/src/SI/ROOT b/src/SI/ROOT old mode 100644 new mode 100755 diff --git a/src/SI/SI.thy b/src/SI/SI.thy old mode 100644 new mode 100755 diff --git a/src/SI/SIOld.thy b/src/SI/SIOld.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Astronomical.thy b/src/SI/SI_Astronomical.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Imperial.thy b/src/SI/SI_Imperial.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy old mode 100644 new mode 100755 diff --git a/src/SI/document/adb-long.bib b/src/SI/document/adb-long.bib old mode 100644 new mode 100755 diff --git a/src/SI/document/root.bib b/src/SI/document/root.bib old mode 100644 new mode 100755 diff --git a/src/SI/document/root.tex b/src/SI/document/root.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-eptcs-UNSUPPORTED.tex b/src/document-templates/root-eptcs-UNSUPPORTED.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex b/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-lncs.tex b/src/document-templates/root-lncs.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrartcl.tex b/src/document-templates/root-scrartcl.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrreprt-modern.tex b/src/document-templates/root-scrreprt-modern.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrreprt.tex b/src/document-templates/root-scrreprt.tex old mode 100644 new mode 100755 diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/DOF-math_exam.sty b/src/ontologies/math_exam/DOF-math_exam.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/Nmath_exam.thy b/src/ontologies/math_exam/Nmath_exam.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/math_exam.thy b/src/ontologies/math_exam/math_exam.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_paper/math_paper.thy b/src/ontologies/math_paper/math_paper.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/ontologies.thy b/src/ontologies/ontologies.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/technical_report/DOF-technical_report.sty b/src/ontologies/technical_report/DOF-technical_report.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy old mode 100644 new mode 100755 diff --git a/src/patches/thy_output.Isabelle2020.ML b/src/patches/thy_output.Isabelle2020.ML old mode 100644 new mode 100755 diff --git a/src/patches/thy_output.ML b/src/patches/thy_output.ML old mode 100644 new mode 100755 diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy old mode 100644 new mode 100755 diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy old mode 100644 new mode 100755 diff --git a/src/tests/Concept_Example.thy b/src/tests/Concept_Example.thy old mode 100644 new mode 100755 diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_ExampleInvariant.thy old mode 100644 new mode 100755 diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/InnerSyntaxAntiquotations.thy old mode 100644 new mode 100755 diff --git a/src/tests/ROOT b/src/tests/ROOT old mode 100644 new mode 100755 diff --git a/src/tests/figures/A.png b/src/tests/figures/A.png old mode 100644 new mode 100755 diff --git a/src/tests/figures/AnB.odp b/src/tests/figures/AnB.odp old mode 100644 new mode 100755 diff --git a/src/tests/figures/B.png b/src/tests/figures/B.png old mode 100644 new mode 100755