meta ?MetaAnnotations?problemTheory ?Midpoint2/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Midpoint2/Solution ❙
theory Test =
meta ?MetaAnnotations?problemTheory ?Test/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Test/Solution ❙
theory Problem =
P: point
❘ meta ?MetaAnnotations?label "P"
...
...
@@ -16,13 +16,13 @@ theory Midpoint2 =
❙
❚
theory Solution =
include ?Midpoint2/Problem ❙
meta ?MetaAnnotations?label "Midpoint2" ❙
meta ?MetaAnnotations?description s"Our Midpoint2 scroll that given two points ${lverb P} and ${lverb Q} computes the Midpoint2 of the line ${lverb P Q}." ❙
Midpoint2: point
include ?Test/Problem ❙
meta ?MetaAnnotations?label "Test" ❙
meta ?MetaAnnotations?description s"Our Test scroll that given two points ${lverb P} and ${lverb Q} computes the Test of the line ${lverb P Q}." ❙