diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/DiffApp-oldscr.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,96 @@
+(*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
+
+(* Das erste Script aus dem Maximum-Beispiel.
+   parse erzeugt aus dem string 's' den 
+  'cterm 's' im Isabelle-Format (pretty-printing !)*)
+
+ML> ...
+ML> val c = (the o (parse thy)) s; 
+val c =
+  "Script1 Maximum_value fix_ m_ rs_ v_ itv_ err_ =
+    let e_ = (hd o filter (Testvar m_)) rs_;
+        t_ =
+          if #1 < Length rs_
+          then make_fun (R, [make, function], no_met) m_ v_ rs_
+          else (Lhs o hd) rs_;
+        mx_ =
+          max_on_interval (R, [on_interval, max_of, function],
+                           maximum_on_interval) t_ v_ itv_
+    in find_vals (R, [find_values, tool], find_values)
+       mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
+
+ML> set show_types;
+ML> c;
+val c =
+  "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_::real itv_::real set err_::bool =
+    let e_::bool = (hd o filter (Testvar m_)) rs_;
+        t_::real =
+          if (#1::real) < Length rs_
+          then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_ rs_
+          else (Lhs o hd) rs_;
+        mx_::real =
+          max_on_interval (R, [on_interval::ID, max_of::ID, function],
+                           maximum_on_interval::ID) t_ v_ itv_
+    in find_vals (R, [find_values::ID, tool::ID], find_values)
+       mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
+
+
+
+(* Die ersten 3 Scripts aus dem Maximum-Beispiel.
+   parse erzeugt aus dem string 's' den 
+  'cterm 's' im Isabelle-Format (pretty-printing !)*)
+
+ML> ...
+ML> val c = (the o (parse thy)) s; 
+val c =
+  "Script maximum =
+    Input [Bool fix_, Real m_, BoolList rs_, Real v_, RealSet itv_, Bool err_]
+    Local [Bool e_, Real t_, Real mx_, RealList vs_]
+    Tacs [SEQU
+           [let e_ = (hd o filter (Testvar m_)) rs_
+            in if #1 < Length rs_
+               then Subproblem Spec (R, [make, function], no_met)
+                     InOut [In m_, In v_, In rs_, Out t_]
+               else t_ := (Lhs o hd) rs_ ;
+            Subproblem Spec (R, [on_interval, max_of, function],
+                             maximum_on_interval)
+             InOut [In t_, In v_, In itv_, In err_, Out mx_] ;
+            Subproblem Spec (R, [find_values, tool], find_values)
+             InOut [In mx_, In t_, In v_, In m_, In (dropWhile (op = e_) rs_),
+                    Out vs_]]]
+    Return []" : cterm
+
+ML> ...
+ML> val c = (the o (parse thy)) s; 
+val c =
+  "Script make_fun_by_new_variable =
+    Input [Real f_, Real v_, BoolList eqs_]
+    Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
+           Bool e2_, BoolList s_1, BoolList s_2]
+    Tacs [SEQU
+           [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];
+                vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
+                e1_ = (hd o filter (Testvar v1_)) es_;
+                e2_ = (hd o filter (Testvar v2_)) es_
+            in Subproblem Spec (R, [univar, equation], no_met)
+                InOut [In e1_, In v1_, Out s_1] ;
+               Subproblem Spec (R, [univar, equation], no_met)
+                InOut [In e2_, In v2_, Out s_2]],
+          Take (Bool h_) ;
+          Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
+    Return [Currform]" : cterm
+
+ML> ...
+ML> val c = (the o (parse thy)) s; 
+val c =
+  "Script make_fun_explicit =
+    Input [Real f_, Real v_, BoolList eqs_]
+    Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
+    Tacs [SEQU
+           [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);
+                vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
+            in Subproblem Spec (R, [univar, equation], no_met)
+                InOut [In eq_, In v1_, Out ss_]],
+          Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
+    Return [Currform]" : cterm
+ML>