diff --git a/upstream_afp/Isabelle_DOF/document/figures/src/document-hierarchy.svg b/upstream_afp/Isabelle_DOF/document/figures/src/document-hierarchy.svg new file mode 100644 index 0000000..f4b2f4b --- /dev/null +++ b/upstream_afp/Isabelle_DOF/document/figures/src/document-hierarchy.svg @@ -0,0 +1,660 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + context definition + A + + + header + + command + + command + + command + + + context definition + C + + header + + command + + command + + command + + + context definition + B + + header + + command + + command + + command + + + context definition + D + + header + + command + + command + + command + + + + + diff --git a/upstream_afp/Isabelle_DOF/document/figures/src/document-model.key b/upstream_afp/Isabelle_DOF/document/figures/src/document-model.key new file mode 100755 index 0000000..f06596b Binary files /dev/null and b/upstream_afp/Isabelle_DOF/document/figures/src/document-model.key differ diff --git a/upstream_afp/Isabelle_DOF/document/figures/src/document-model.pptx b/upstream_afp/Isabelle_DOF/document/figures/src/document-model.pptx new file mode 100644 index 0000000..16932b3 Binary files /dev/null and b/upstream_afp/Isabelle_DOF/document/figures/src/document-model.pptx differ diff --git a/upstream_afp/Isabelle_DOF/document/figures/src/isabelle-architecture.svg b/upstream_afp/Isabelle_DOF/document/figures/src/isabelle-architecture.svg new file mode 100644 index 0000000..eda1a04 --- /dev/null +++ b/upstream_afp/Isabelle_DOF/document/figures/src/isabelle-architecture.svg @@ -0,0 +1,1115 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + + PIDE SCALA + PIDE SML + Editor Front-End + Isabelle + evaluation + approx. display + edits + markup + + + + + Editor Front-End + Isabelle + + (e.g., JEdit, VSCode, Eclipse) + + PIDE + SML Environment + + + Integrators + (e.g., sledgehammer) + Project & DependencyManagement + + + CodeGenerator + + DocumentGenerator + + Components + (e.g., datatype, record) + + Tactic Procedures + (e.g., simp, fast, metis) + + Kernel + (e.g., typ, term, thm,thy) + + Nano-Kernel + (e.g., context) + + Z3 + + . . . + + CVC4 + + PDF/LaTeX + + . . . + + HTML + + Haskell + + . . . + + Scala + + + + + + + + + + +