From 0e3e079349b3d6fc068dab974568b02e4960e48e Mon Sep 17 00:00:00 2001 From: Michael Kohlhase <michael.kohlhase@fau.de> Date: Tue, 27 Oct 2020 07:43:17 +0100 Subject: [PATCH] adding a comment on scroll meta-annotations --- source/Scrolls/README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md index 90be86b..ed57bae 100644 --- a/source/Scrolls/README.md +++ b/source/Scrolls/README.md @@ -33,6 +33,9 @@ theory Midpoint = to have access to the facts formalized in the problem theory â™ include ?Midpoint/Problem â™ + // the next meta annotations (to the theory) actually make this theory into a scroll: + We specify the Problem and Solution theories â™ + meta ?MetaAnnotations?label "MidPoint" â™ meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™ meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution â™ @@ -58,4 +61,4 @@ theory Midpoint = â™ âš âš -``` \ No newline at end of file +``` -- GitLab