refactor StepUntil into dynamics.mmt

build.msl

 build FrameIT/frameworld mmt-omdoc MetaTheories.mmt
+build FrameIT/frameworld scala-bin
+build FrameIT/frameworld mmt-omdoc dynamics.mmt
 build FrameIT/frameworld mmt-omdoc Scrolls/
 build FrameIT/frameworld mmt-omdoc DefaultSituationSpace.mmt

frameworld.iml

+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager">
+    <output url="file://$MODULE_DIR$/bin" />
+    <exclude-output />
+    <content url="file://$MODULE_DIR$">
+      <sourceFolder url="file://$MODULE_DIR$/scala" isTestSource="false" />
+      <excludeFolder url="file://$MODULE_DIR$/bin" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="module" module-name="mmt-api" />
+    <orderEntry type="module" module-name="mmt-lf" />
+    <orderEntry type="module" module-name="LFX" />
+    <orderEntry type="library" name="scala-sdk-2.13.1" level="application" />
+  </component>
+</module>
\ No newline at end of file

source/.idea/source.iml

-<?xml version="1.0" encoding="UTF-8"?>
-<module type="JAVA_MODULE" version="4">
-  <component name="NewModuleRootManager" inherit-compiler-output="true">
-    <exclude-output />
-    <content url="file://$MODULE_DIR$" />
-    <orderEntry type="inheritedJdk" />
-    <orderEntry type="sourceFolder" forTests="false" />
-  </component>
-</module>
\ No newline at end of file

source/Scrolls/BouncingScroll.mmt

@@ -2,16 +2,9 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 
 import base http://mathhub.info/MitM/Foundation ❚
 import arith http://mathhub.info/MitM/core/arithmetics ❚
-//import rules scala://datatypes.LFX.mmt.kwarc.info ❚
 import rules scala://rules.frameit.mmt.kwarc.info ❚
-//fixmeta base:?Logic ❚
 fixmeta ?FrameworldMeta ❚
 
-theory StepUntilWrap =
-    stepUntil : ℝ ⟶ (ℝ ⟶ ℝ) ⟶ (ℝ ⟶ bool) ⟶ List[ℝ] ❘ # stepUntil 1 2 3 ❙
-    rule rules?StepUntilRule (true) ❙
-❚
-
 theory BouncingScroll =
     meta ?MetaAnnotations?problemTheory ?BouncingScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?BouncingScroll/Solution ❙

source/Scrolls/SupplementaryAngles.mmt

@@ -8,10 +8,10 @@ fixmeta ?FrameworldMeta ❚
  ________\_________
 A         B        C
 
-The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD"
+The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD".
 ❚
 theory SupplementaryAngles =
-    meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem ❙
+    meta ?MetaAnnotations?problemTheory  ?SupplementaryAngles/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/Solution ❙
 
     theory Problem =

source/dynamics.mmt

+namespace http://mathhub.info/FrameIT/frameworld ❚
+
+import base http://mathhub.info/MitM/Foundation ❚
+import arith http://mathhub.info/MitM/core/arithmetics ❚
+import rules scala://rules.frameit.mmt.kwarc.info ❚
+fixmeta ?FrameworldMeta ❚
+
+theory StepUntilWrap =
+    stepUntil: ℝ ⟶ (ℝ ⟶ ℝ) ⟶ (ℝ ⟶ bool) ⟶ List[ℝ] ❘ # stepUntil 1 2 3 ❙
+    rule rules?StepUntilRule (true) ❙
+❚
+