1.1 --- a/doc/isac-docu.tex Thu May 10 11:06:34 2007 +0200
1.2 +++ b/doc/isac-docu.tex Thu May 17 12:31:32 2007 +0200
1.3 @@ -13,6 +13,7 @@
1.4 {\tt isac@ist.tugraz.at}\\
1.5 {\tt www.ist.tugraz.at/projects/isac}}
1.6 \date{$Revision$}
1.7 +%\date{$Revision$}WN070420 work of GK RK NC integrated
1.8 %\date{$Revision$}WN060707 marked entry-points for GK RK SC
1.9 %\date{$Revision$}WN060704 after ML, before GK RK SC, design patterns!
1.10 %\date{$Revision$}WN040417 entered all papernotes
2.1 --- a/src/sml/IsacKnowledge/Atools.thy Thu May 10 11:06:34 2007 +0200
2.2 +++ b/src/sml/IsacKnowledge/Atools.thy Thu May 17 12:31:32 2007 +0200
2.3 @@ -42,7 +42,7 @@
2.4 "argument'_in" :: real => real ("argument'_in _" 10)
2.5 "sameFunId" :: [real, bool] => bool (**"same'_funid _ _" 10
2.6 WN0609 changed the id, because ".. _ _" inhibits currying**)
2.7 - "filter'_sameFunId":: [real, bool list] => real list
2.8 + "filter'_sameFunId":: [real, bool list] => bool list
2.9 ("filter'_sameFunId _ _" 10)
2.10 "boollist2sum" :: bool list => real
2.11
3.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Thu May 10 11:06:34 2007 +0200
3.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Thu May 17 12:31:32 2007 +0200
3.3 @@ -154,8 +154,10 @@
3.4 Calc("op +", eval_binop "#add_"),
3.5 Thm ("nth_Nil_", num_str nth_Nil_),
3.6 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
3.7 - Calc("Atools.sameFunId",
3.8 - eval_sameFunId "Atools.sameFunId"),
3.9 + Calc("Atools.filter'_sameFunId",
3.10 + eval_filter_sameFunId "Atools.filter'_sameFunId"),
3.11 + (*WN070514 just for smltest/../biegelinie.sml ...*)
3.12 + Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
3.13 Thm ("filter_Cons", num_str filter_Cons),
3.14 Thm ("filter_Nil", num_str filter_Nil),
3.15 Thm ("if_True", num_str if_True),
3.16 @@ -383,31 +385,31 @@
3.17 crls = Atools_erls, nrls = e_rls},
3.18 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
3.19 \ (let b1_ = nth_ 1 rb_; \
3.20 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
3.21 +\ fs_ = filter_sameFunId (lhs b1_) funs_; \
3.22 \ (e1_::bool) = \
3.23 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
3.24 \ [Equation,fromFunction]) \
3.25 \ [bool_ (hd fs_), bool_ b1_]); \
3.26 \ b2_ = nth_ 2 rb_; \
3.27 -\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
3.28 +\ fs_ = filter_sameFunId (lhs b2_) funs_; \
3.29 \ (e2_::bool) = \
3.30 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
3.31 \ [Equation,fromFunction]) \
3.32 \ [bool_ (hd fs_), bool_ b2_]); \
3.33 \ b3_ = nth_ 3 rb_; \
3.34 -\ fs_ = filter (sameFunId (lhs b3_)) funs_; \
3.35 +\ fs_ = filter_sameFunId (lhs b3_) funs_; \
3.36 \ (e3_::bool) = \
3.37 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
3.38 \ [Equation,fromFunction]) \
3.39 \ [bool_ (hd fs_), bool_ b3_]); \
3.40 \ b4_ = nth_ 4 rb_; \
3.41 -\ fs_ = filter (sameFunId (lhs b4_)) funs_; \
3.42 +\ fs_ = filter_sameFunId (lhs b4_) funs_; \
3.43 \ (e4_::bool) = \
3.44 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
3.45 \ [Equation,fromFunction]) \
3.46 \ [bool_ (hd fs_), bool_ b4_]) \
3.47 \ in [e1_,e2_,e3_,e4_])"
3.48 -(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
3.49 +(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
3.50 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
3.51 \ (let b1_ = nth_ 1 rb_; \
3.52 \ fs_ = filter (sameFunId (lhs b1_)) funs_; \
4.1 --- a/src/sml/IsacKnowledge/Diff.ML Thu May 10 11:06:34 2007 +0200
4.2 +++ b/src/sml/IsacKnowledge/Diff.ML Thu May 17 12:31:32 2007 +0200
4.3 @@ -30,6 +30,48 @@
4.4
4.5 (** rulesets **)
4.6
4.7 +val diff_conv =
4.8 + Rls {id="diff_conv",
4.9 + preconds = [],
4.10 + rew_ord = ("termlessI",termlessI),
4.11 + erls = append_rls "erls_diff_conv" e_rls
4.12 + [Calc ("Atools.occurs'_in", eval_occurs_in ""),
4.13 + Thm ("not_true",num_str not_true),
4.14 + Thm ("not_false",num_str not_false)
4.15 + ],
4.16 + srls = Erls, calc = [],
4.17 + rules = [Thm ("frac_conv", num_str frac_conv),
4.18 + Thm ("sqrt_conv", num_str sqrt_conv),
4.19 + Thm ("root_conv", num_str root_conv),
4.20 + Thm ("realpow_pow", num_str realpow_pow),
4.21 + Calc ("op *", eval_binop "#mult_"),
4.22 + Thm ("rat_mult",num_str rat_mult),
4.23 + (*a / b * (c / d) = a * c / (b * d)*)
4.24 + Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
4.25 + (*?x * (?y / ?z) = ?x * ?y / ?z*)
4.26 + Thm ("real_times_divide2_eq",num_str real_times_divide2_eq)
4.27 + (*?y / ?z * ?x = ?y * ?x / ?z*)
4.28 + (*
4.29 + Thm ("", num_str ),*)
4.30 + ],
4.31 + scr = EmptyScr};
4.32 +val diff_sym_conv =
4.33 + Rls {id="diff_sym_conv",
4.34 + preconds = [],
4.35 + rew_ord = ("termlessI",termlessI),
4.36 + erls = append_rls "erls_diff_sym_conv" e_rls
4.37 + [Calc ("op <",eval_equ "#less_")
4.38 + ],
4.39 + srls = Erls, calc = [],
4.40 + rules = [Thm ("frac_sym_conv", num_str frac_sym_conv),
4.41 + Thm ("sqrt_sym_conv", num_str sqrt_sym_conv),
4.42 + Thm ("root_sym_conv", num_str root_sym_conv),
4.43 + Thm ("sym_real_mult_minus1",
4.44 + num_str (real_mult_minus1 RS sym))
4.45 + (*- ?z = "-1 * ?z"*)
4.46 + ],
4.47 + scr = EmptyScr};
4.48 +
4.49 val srls_diff =
4.50 Rls {id="srls_differentiate..",
4.51 preconds = [],
4.52 @@ -70,8 +112,10 @@
4.53 Thm ("diff_ln_chain",num_str diff_ln_chain),
4.54 Thm ("diff_exp",num_str diff_exp),
4.55 Thm ("diff_exp_chain",num_str diff_exp_chain),
4.56 +(*
4.57 Thm ("diff_sqrt",num_str diff_sqrt),
4.58 Thm ("diff_sqrt_chain",num_str diff_sqrt_chain),
4.59 +*)
4.60 Thm ("diff_const",num_str diff_const),
4.61 Thm ("diff_var",num_str diff_var),
4.62 Rls_ norm_Poly
4.63 @@ -128,6 +172,7 @@
4.64 "Script DiffScr (f_::real) (v_::real) = \
4.65 \ (let f'_ = Take (d_d v_ f_) \
4.66 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
4.67 + \ (Try (Repeat (Rewrite sqrt_conv False))) @@ \
4.68 \ (Try (Repeat (Rewrite root_conv False))) @@ \
4.69 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
4.70 \ (Repeat \
4.71 @@ -145,12 +190,11 @@
4.72 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
4.73 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
4.74 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
4.75 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
4.76 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
4.77 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
4.78 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
4.79 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
4.80 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
4.81 + \ (Try (Repeat (Rewrite sym_sqrt_conv False))) @@ \
4.82 \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)"
4.83 ));
4.84
4.85 @@ -178,8 +222,6 @@
4.86 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
4.87 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
4.88 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
4.89 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
4.90 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
4.91 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
4.92 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
4.93 \ (Repeat (Rewrite_Set make_polynomial False)))) \
4.94 @@ -197,6 +239,7 @@
4.95 "Script DiffEqScr (f_::bool) (v_::real) = \
4.96 \ (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_)) \
4.97 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
4.98 + \ (Try (Repeat (Rewrite sqrt_conv False))) @@ \
4.99 \ (Try (Repeat (Rewrite root_conv False))) @@ \
4.100 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
4.101 \ (Repeat \
4.102 @@ -215,12 +258,11 @@
4.103 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
4.104 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
4.105 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
4.106 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
4.107 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
4.108 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
4.109 \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
4.110 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
4.111 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
4.112 + \ (Try (Repeat (Rewrite sym_sqrt_conv False))) @@ \
4.113 \ (Try (Repeat (Rewrite sym_root_conv False))) @@ \
4.114 \ (Try (Repeat (Rewrite sym_real_diff_minus False))) @@ \
4.115 \ (Try (Repeat (Rewrite real_mult_minus1 False))))) f'_)"
5.1 --- a/src/sml/IsacKnowledge/Diff.thy Thu May 10 11:06:34 2007 +0200
5.2 +++ b/src/sml/IsacKnowledge/Diff.thy Thu May 17 12:31:32 2007 +0200
5.3 @@ -3,6 +3,7 @@
5.4 000516
5.5
5.6 remove_thy"Diff";
5.7 +use_thy_only"IsacKnowledge/Diff";
5.8 use_thy"IsacKnowledge/Isac";
5.9 *)
5.10
5.11 @@ -59,12 +60,19 @@
5.12 diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u"
5.13 diff_exp "d_d bdv (exp bdv) = exp bdv"
5.14 diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u"
5.15 +(*
5.16 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
5.17 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
5.18 +*)
5.19 (*...*)
5.20
5.21 - frac_conv "a is_const ==> a / b = a * b ^^^ (-1)"
5.22 - root_conv "nroot n u = u ^^^ (1 / n)"
5.23 + frac_conv "[| Not (bdv occurs_in a); bdv occurs_in b |] ==> \
5.24 + \ a / b = a * b ^^^ (-1)"
5.25 + frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
5.26 + sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
5.27 + sqrt_sym_conv "u ^^^ (a / 2) = sqrt (a ^^^ n)"
5.28 + root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
5.29 + root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)"
5.30
5.31 end
5.32
6.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Thu May 10 11:06:34 2007 +0200
6.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Thu May 17 12:31:32 2007 +0200
6.3 @@ -19,7 +19,8 @@
6.4 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
6.5 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
6.6 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
6.7 -"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
6.8 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
6.9 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
6.10 "----------- investigate normalforms in biegelinien --------------";
6.11 "-----------------------------------------------------------------";
6.12 "-----------------------------------------------------------------";
6.13 @@ -842,9 +843,58 @@
6.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.15 *)
6.16
6.17 -"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
6.18 -"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
6.19 -"----------- IntegrierenUndKonstanteBestimmen2 -------------------";
6.20 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
6.21 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
6.22 +"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
6.23 +(*---^^^-OK-----------------------------------------------------------------*)
6.24 +(*---vvv-NOTok--------------------------------------------------------------*)
6.25 +val str =
6.26 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
6.27 +\ (let b1_ = nth_ 1 rb_; \
6.28 +\ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
6.29 +\ (e1_::bool) = \
6.30 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
6.31 +\ [Equation,fromFunction]) \
6.32 +\ [bool_ (hd fs_), bool_ b1_]) \
6.33 +\ in [e1_,e2_,e3_,e4_])"
6.34 +;
6.35 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
6.36 +(*---vvv-NOTok--------------------------------------------------------------*)
6.37 +val str =
6.38 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
6.39 +\ (let b1_ = nth_ 1 rb_; \
6.40 +\ fs_ = filter_sameFunId (lhs b1_) funs_; \
6.41 +\ (e1_::bool) = \
6.42 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
6.43 +\ [Equation,fromFunction]) \
6.44 +\ [bool_ (hd fs_), bool_ b1_]); \
6.45 +\ b2_ = nth_ 2 rb_; \
6.46 +\ fs_ = filter_sameFunId (lhs b2_) funs_; \
6.47 +\ (e2_::bool) = \
6.48 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
6.49 +\ [Equation,fromFunction]) \
6.50 +\ [bool_ (hd fs_), bool_ b2_]); \
6.51 +\ b3_ = nth_ 3 rb_; \
6.52 +\ fs_ = filter_sameFunId (lhs b3_) funs_; \
6.53 +\ (e3_::bool) = \
6.54 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
6.55 +\ [Equation,fromFunction]) \
6.56 +\ [bool_ (hd fs_), bool_ b3_]); \
6.57 +\ b4_ = nth_ 4 rb_; \
6.58 +\ fs_ = filter_sameFunId (lhs b4_) funs_; \
6.59 +\ (e4_::bool) = \
6.60 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
6.61 +\ [Equation,fromFunction]) \
6.62 +\ [bool_ (hd fs_), bool_ b4_]) \
6.63 +\ in [e1_,e2_,e3_,e4_])"
6.64 +;
6.65 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
6.66 +
6.67 +
6.68 +
6.69 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
6.70 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
6.71 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
6.72 "----- script ";
6.73 val str =
6.74 "Script Belastung2BiegelScript (q__::real) (v_::real) = \
6.75 @@ -920,9 +970,12 @@
6.76 ["IntegrierenUndKonstanteBestimmen2"]))];
6.77 moveActiveRoot 1;
6.78 autoCalculate 1 CompleteCalc;
6.79 -val ((pt,_),_) = get_calc 1;show_pt pt;
6.80 +val ((pt,p),_) = get_calc 1; show_pt pt;
6.81 +if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
6.82 +"y x =\n-6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +\n4 * L * q_0 / (-24 * EI) * x ^^^ 3 +\n-1 * q_0 / (-24 * EI) * x ^^^ 4" then ()
6.83 +else raise error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
6.84 +
6.85 val is = get_istate pt ([],Res); writeln (istate2str is);
6.86 -
6.87 val t = str2term " last \
6.88 \[Q x = L * q_0 + -1 * q_0 * x, \
6.89 \ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
7.1 --- a/src/smltest/IsacKnowledge/diff.sml Thu May 10 11:06:34 2007 +0200
7.2 +++ b/src/smltest/IsacKnowledge/diff.sml Thu May 17 12:31:32 2007 +0200
7.3 @@ -16,6 +16,8 @@
7.4 " _________________ differentiate stdin: tutor active_________________ ";
7.5 "---------------------1.5.02 me from script ---------------------";
7.6 "----------- primed id -------------------------------------------";
7.7 +"----------- diff_conv, sym_diff_conv ----------------------------";
7.8 +"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
7.9 "----------- autoCalculate differentiate_equality ----------------";
7.10 "----------- tests for examples ----------------------------------";
7.11 "-----------------------------------------------------------------";
7.12 @@ -62,6 +64,7 @@
7.13 Thm ("or_commute",num_str or_commute),
7.14
7.15 Calc ("Atools.is'_const",eval_const "#is_const_"),
7.16 + Calc ("Atools.occurs'_in", eval_occurs_in ""),
7.17 Calc ("Tools.matches",eval_matches ""),
7.18
7.19 Calc ("op +",eval_binop "#add_"),
7.20 @@ -165,7 +168,8 @@
7.21 val thm = ("diff_var","");
7.22 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.23 [("bdv","x::real")] thm ct);
7.24 -"2 * x ^^^ (2 - 1) + 3 * 1 + 0";
7.25 +if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
7.26 +else raise error "diff.sml diff.behav. in rewrite 1";
7.27 "--- 7 ---";
7.28 val rls = ("Test_simplify");
7.29 val (ct,_) = the (rewrite_set thy' false rls ct);
7.30 @@ -506,6 +510,53 @@
7.31 ;
7.32 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.33
7.34 +
7.35 +"----------- diff_conv, sym_diff_conv ----------------------------";
7.36 +"----------- diff_conv, sym_diff_conv ----------------------------";
7.37 +"----------- diff_conv, sym_diff_conv ----------------------------";
7.38 +val rls = diff_conv; val subs = [(str2term "bdv", str2term "x")];
7.39 +
7.40 +val t = str2term "2/x^^^2";
7.41 +val Some (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
7.42 +if term2str t = "2 * x ^^^ -2" then () else raise error "diff.sml 1/x";
7.43 +
7.44 +val t = str2term "sqrt x^^^3";
7.45 +val Some (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
7.46 +if term2str t = "x ^^^ (3 / 2)" then () else raise error "diff.sml xT^1/2";
7.47 +
7.48 +val t = str2term "2 / sqrt x^^^3";
7.49 +val Some (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
7.50 +if term2str t = "2 * x ^^^ (-3 / 2)" then () else raise error"diff.sml x^-1/2";
7.51 +
7.52 +val rls = diff_sym_conv;
7.53 +
7.54 +val t = str2term "2 * x ^^^ -2";
7.55 +val Some (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
7.56 +
7.57 +(* trace_rewrite:=true;
7.58 + *)
7.59 +(* trace_rewrite:=false;
7.60 + *)
7.61 +(*@@@@*)
7.62 +
7.63 +
7.64 +"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
7.65 +"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
7.66 +"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
7.67 +states:=[];
7.68 +CalcTree
7.69 +[([(*"functionTerm (x^2 + x+ 1/x + 2/x^2)",*)
7.70 + "functionTerm (2/x^2)",
7.71 + "differentiateFor x", "derivative f_'_"],
7.72 + ("Isac.thy", ["derivative_of","function"],
7.73 + ["diff","differentiate_on_R"]))];
7.74 +Iterator 1;
7.75 +moveActiveRoot 1;
7.76 +autoCalculate 1 CompleteCalc;
7.77 +val ((pt,p),_) = get_calc 1; show_pt pt;
7.78 +
7.79 +
7.80 +
7.81 "----------- autoCalculate differentiate_equality ----------------";
7.82 "----------- autoCalculate differentiate_equality ----------------";
7.83 "----------- autoCalculate differentiate_equality ----------------";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/xmldata/users/README-users.txt Thu May 17 12:31:32 2007 +0200
8.3 @@ -0,0 +1,24 @@
8.4 +README-users.txt
8.5 +WN070510
8.6 +
8.7 +[nb] cd ~/proto2/isac/xmldata/users
8.8 +----------------------------------------------------------------------
8.9 +how to implement new users on the isacserver:
8.10 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8.11 +> emacs accounts.txt &
8.12 + + add: username=password
8.13 +> cp x_admin.txt ..._admin.txt
8.14 +> cp x_model.txt ..._model.txt
8.15 +> cp x_settings.txt ..._settings.txt
8.16 +----------------------------------------------------------------------
8.17 +copy new users to ist (immediate copy to dmz is not possible)
8.18 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8.19 +> scp -r * wneuper@pear.ist.intra:/netshares/commons/isac/proto2-isacserver/xmldata/users
8.20 +----------------------------------------------------------------------
8.21 +copy new users to isac@...dmz
8.22 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8.23 +> ssh ist
8.24 +> cd /netshares/commons/isac/proto2-isacserver/xmldata/users
8.25 +> scp -r * isac@isac.ist.dmz:/home/isac/proto2-isacserver/xmldata/users
8.26 + SzEWS/Ce
8.27 +----------------------------------------------------------------------
9.1 --- a/xmldata/users/accounts.txt Thu May 10 11:06:34 2007 +0200
9.2 +++ b/xmldata/users/accounts.txt Thu May 17 12:31:32 2007 +0200
9.3 @@ -3,4 +3,6 @@
9.4 x=x
9.5 anonymous=anonymous
9.6 y=y
9.7 -a=a
9.8 \ No newline at end of file
9.9 +a=a
9.10 +winkelbauer=johannes
9.11 +krempler=alan
9.12 \ No newline at end of file
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/xmldata/users/krempler_admin.txt Thu May 17 12:31:32 2007 +0200
10.3 @@ -0,0 +1,4 @@
10.4 +#administrative data of user 'x'
10.5 +#Sat Mar 12 09:05:42 CET 2005
10.6 +lastName=krempler
10.7 +firstName=alan
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/xmldata/users/krempler_model.txt Thu May 17 12:31:32 2007 +0200
11.3 @@ -0,0 +1,3 @@
11.4 +#dynamic dialog data of user 'x'
11.5 +#WN070510
11.6 +TODO-key=TODO-value
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/xmldata/users/krempler_settings.txt Thu May 17 12:31:32 2007 +0200
12.3 @@ -0,0 +1,6 @@
12.4 +#static dialog data of user 'winkelbauer' creating 'short calculations'
12.5 +#WN070510
12.6 +KEY1_START_SPECIFY=VAL1_SKIP_SPECIFY_TO_START_SOLVE
12.7 +KEY2_NEXT_BUTTON=VAL2_FORMULAE_ONLY
12.8 +KEY3_STATUS=VAL3_LEARNER
12.9 +KEY4_LANGUAGE=VAL4_ENGLISH
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/xmldata/users/winkelbauer_admin.txt Thu May 17 12:31:32 2007 +0200
13.3 @@ -0,0 +1,4 @@
13.4 +#administrative data of user 'x'
13.5 +#WN070510
13.6 +lastName=winkelbauer
13.7 +firstName=johannes
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/xmldata/users/winkelbauer_model.txt Thu May 17 12:31:32 2007 +0200
14.3 @@ -0,0 +1,3 @@
14.4 +#dynamic dialog data of user 'x'
14.5 +#WN070510
14.6 +TODO-key=TODO-value
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/xmldata/users/winkelbauer_settings.txt Thu May 17 12:31:32 2007 +0200
15.3 @@ -0,0 +1,6 @@
15.4 +#static dialog data of user 'x' creating 'short calculations'
15.5 +#WN070510
15.6 +KEY1_START_SPECIFY=VAL1_SKIP_SPECIFY_TO_START_SOLVE
15.7 +KEY2_NEXT_BUTTON=VAL2_FORMULAE_ONLY
15.8 +KEY3_STATUS=VAL3_LEARNER
15.9 +KEY4_LANGUAGE=VAL4_ENGLISH
16.1 --- a/xmldata/users/x_model.txt Thu May 10 11:06:34 2007 +0200
16.2 +++ b/xmldata/users/x_model.txt Thu May 17 12:31:32 2007 +0200
16.3 @@ -1,3 +1,3 @@
16.4 #dynamic dialog data of user 'x'
16.5 -#Sat Mar 12 09:20:14 CET 2005
16.6 +#WN070510
16.7 TODO-key=TODO-value
17.1 --- a/xmldata/users/x_settings.txt Thu May 10 11:06:34 2007 +0200
17.2 +++ b/xmldata/users/x_settings.txt Thu May 17 12:31:32 2007 +0200
17.3 @@ -1,5 +1,5 @@
17.4 -#static dialog data of user 'x' creating 'short calculations'
17.5 -#Sat Mar 12 11:16:11 CET 2005
17.6 +#static dialog data of user 'winkelbauer' creating 'short calculations'
17.7 +#WN070510
17.8 KEY1_START_SPECIFY=VAL1_SKIP_SPECIFY_TO_START_SOLVE
17.9 KEY2_NEXT_BUTTON=VAL2_FORMULAE_ONLY
17.10 KEY3_STATUS=VAL3_LEARNER