diff -r 7e314dd233fd -r 46fe5a8c3911 src/Tools/isac/Knowledge/DiffApp-oldpbl.sml
--- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Tue May 19 12:33:35 2020 +0200
+++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml	Wed May 20 12:52:09 2020 +0200
@@ -7,7 +7,7 @@
 (1) names of the problem-types and methods and their hierarchy
     as subproblems.
     names of problem-types are string lists (diss 5.3.), not shown
-    here with exception of ["equation","univariate"] in order to
+    here with exception of ["equation", "univariate"] in order to
     indicate, that this particular problem needs refinement to a
     more specific type of equation solvable by tan-square, etc.
 
@@ -19,7 +19,7 @@
                                   introduce-a-new-variable
   max-of-fun-on-interval          max-of-fun-on-interval
     derivative                    differentiate
-    ["equation","univariate"]     tan-square
+    ["equation", "univariate"]     tan-square
                                   
   find-values                     find-values
 
@@ -32,11 +32,11 @@
 {given = ["fixed_values (cs::bool list)"],
  where_= ["foldl (op &) True (map is_equality cs)",
 	  "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
- find=["maximum m","values_for (ms::real list)"],
+ find=["maximum m", "values_for (ms::real list)"],
  with_=["Ex_frees ((foldl (op &) True (r#RS)) &       \
   \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \
   \            --> m' <= m)))"],
- relate=["max_relation r","additionalRels RS"]};
+ relate=["max_relation r", "additionalRels RS"]};
 (* ^^^ is exponenation *)
 
 (* the functions Ex_frees, Rhs provide for the instantiation below *)
@@ -45,7 +45,7 @@
 {given = ["fixed_values (R = #7)"],
  where_= ["is_equality (R = #7)",
 	  "Not (R <= #0)"],
- find  =["maximum A","values_for [a,b]"],
+ find  =["maximum A", "values_for [a,b]"],
  with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
   \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2   \
   \            --> A' <= A)))"],
@@ -57,7 +57,7 @@
 {given = ["fixed_values (R = #7)"],
  where_= ["is_equality (R = #7)",
 	  "Not (R <= #0)"],
- find  =["maximum A","values_for [A]"],
+ find  =["maximum A", "values_for [A]"],
  with_ =["EX a b alpha. A = a*b &                               \
   \                     a = #2*R*sin alpha & b =#2*R*cos alpha &\
   \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha  \
@@ -70,7 +70,7 @@
 (* make-fun *)
 (* -------- *)
 (* problem-type *)
-{given = ["equality (lhs = rhs)","bound_variable v","equalities es"],
+{given = ["equality (lhs = rhs)", "bound_variable v", "equalities es"],
  where_= [],
  find  = ["function_term lhs_"],
  with_ = [(*???*)],
@@ -78,7 +78,7 @@
 (*the _ in lhs is used to transfer the lhs-identifier of equality*)
 
 (* (1) instantiation for make-explicit-and-substitute *)
-{given = ["equality A = a * b","bound_variable a", 
+{given = ["equality A = a * b", "bound_variable a", 
 	  "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"],
  where_= [],
  find  = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
@@ -86,7 +86,7 @@
  relate= []};
 
 (* (2) instantiation for introduce-a-new-variable *)
-{given = ["equality A = a * b","bound_variable alpha", 
+{given = ["equality A = a * b", "bound_variable alpha", 
 	  "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
  where_= [],
  find  = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],
@@ -97,7 +97,7 @@
 (* max-of-fun-on-interval *)
 (* ---------------------- *)
 (* problem-type *)
-{given = ["function_term t","bound_variable v",
+{given = ["function_term t", "bound_variable v",
 	"domain {x::real. lower_bound <= x & x <= upper_bound}"],
  where_= [],
  find  = ["maximums ms"],
@@ -133,7 +133,7 @@
 (* derivative *)
 (* ---------- *)
 (* problem-type *)
-{given = ["function_term t","bound_variable bdv"],
+{given = ["function_term t", "bound_variable bdv"],
  where_= [],
  find  = ["derivative t'"],
  with_ = ["t' is_derivative_of (%bdv. t)"],
@@ -141,11 +141,11 @@
 (*the ' in t' is used to transfer the identifier from function_term*)
 
 
-(* ["equation","univariate"] *)
+(* ["equation", "univariate"] *)
 (* ------------------------- *)
 (* problem-type *)
 {given = ["equality (lhs = rhs)",
-	  "bound_variable v","error_bound eps"],
+	  "bound_variable v", "error_bound eps"],
  where_= [],
  find  = ["solutions S"],
  with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],
@@ -155,7 +155,7 @@
 (* find-values *)
 (* ----------- *)
 (* problem-type *)
-{given = ["max_relation r","additionalRels RS"],
+{given = ["max_relation r", "additionalRels RS"],
  where_= [],
  find  = ["values_for VS"],
  with_ = [(*???*)],
@@ -202,7 +202,7 @@
 
 
 max-of-fun-on-interval + derivative -> 
-                                #given.["equation","univariate"]
+                                #given.["equation", "univariate"]
 ----------------------------------------------------------------
 derivative.#find "derivative t'"         -> "equality (lhs = rhs)"
                                                       (* t'= #0 *)
@@ -231,11 +231,11 @@
 val pbltyp = {given=["fixed_values (cs::bool list)"],
 	      where_=["foldl (op &) True (map is_equality cs)",
 		      "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
-	      find=["maximum m","values_for (ms::real list)"],
+	      find=["maximum m", "values_for (ms::real list)"],
 	      with_=["Ex_frees ((foldl (op &) True (r#rs)) &              \
                       \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
 		      \            --> m' <= m)))"],
-	      relate=["max_relation r","additionalRels rs"]}:string ppc;
+	      relate=["max_relation r", "additionalRels rs"]}:string ppc;
 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
 "coil";
 val org = ["fixed_values [R=(R::real)]", 
@@ -250,7 +250,7 @@
 	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
 val chkorg = map (the o (parse thy)) org;
 val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
-	   find=["maximum A","values_for [a,b]"],
+	   find=["maximum A", "values_for [a,b]"],
 	   with_=["EX alpha. A=#2*a*b - a^^^#2 &    \
 	    \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
 	    \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
@@ -261,12 +261,12 @@
 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
 
 "met --- maximum_by_differentiation ---";
-val met = {given=["fixed_values (cs::bool list)","bound_variable v",
+val met = {given=["fixed_values (cs::bool list)", "bound_variable v",
 		  "domain {x::real. lower_bound <= x & x <= upper_bound}",
 		  "approximation apx"],
 	   where_=[],
-	   find=["maximum m","values_for (ms::real list)",
-		 "function_term t","max_argument mx"],
+	   find=["maximum m", "values_for (ms::real list)",
+		 "function_term t", "max_argument mx"],
 	   with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \
                   \ (ALL m'. (subst (m,m') (foldl (op &) True rs)  \
 		  \            --> m' <= m))) &                    \
@@ -281,13 +281,13 @@
 (* subproblem [(hd #relate root, equality),
                (bound_variable formalization, bound_variable),
 	       (tl #relate root, equalities)] *) 
-val pbltyp = {given=["equality e","bound_variable v", "equalities es"],
+val pbltyp = {given=["equality e", "bound_variable v", "equalities es"],
 	      where_=[],
 	      find=["function_term t"],with_=[(*???*)],
 	      relate=[(*???*)]}: string ppc;
 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
 "coil";
-val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha",
+val pbl = {given=["equality (A=#2*a*b - a^^^#2)", "bound_variable alpha",
 		  "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
 	   where_=[],
 	   find=["function_term t"],
@@ -295,13 +295,13 @@
 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
 
 "met --- make_explicit_and_substitute ---";
-val met = {given=["equality e","bound_variable v", "equalities es"],
+val met = {given=["equality e", "bound_variable v", "equalities es"],
 	   where_=[],
 	   find=["function_term t"],with_=[(*???*)],
 	   relate=[(*???*)]}: string ppc;
 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
 "met --- introduce_a_new_variable ---";
-val met = {given=["equality e","bound_variable v", "substitutions es"],
+val met = {given=["equality e", "bound_variable v", "substitutions es"],
 	   where_=[],
 	   find=["function_term t"],with_=[(*???*)],
 	   relate=[(*???*)]}: string ppc;
@@ -309,7 +309,7 @@
 
 
 "pbltyp --- max_of_fun_on_interval ---";
-val pbltyp = {given=["function_term t","bound_variable v",
+val pbltyp = {given=["function_term t", "bound_variable v",
 		     "domain {x::real. lower_bound <= x & x <= upper_bound}"],
 	      where_=[],
 	      find=["maximums ms"],
@@ -320,7 +320,7 @@
 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
 "coil";
 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
-                   \ (#2*R*sin alpha)^^^#2","bound_variable alpha",
+                   \ (#2*R*sin alpha)^^^#2", "bound_variable alpha",
 		  "domain {x::real. #0 <= x & x <= pi}"],where_=[],
 	   find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;