1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Mon Sep 04 16:56:33 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Tue Sep 05 10:10:27 2006 +0200
1.3 @@ -377,25 +377,25 @@
1.4 prls=e_rls,
1.5 crls = Atools_erls, nrls = e_rls},
1.6 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
1.7 -\ (let b1_ = Take (nth_ 1 rb_); \
1.8 +\ (let b1_ = nth_ 1 rb_; \
1.9 \ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.10 \ (e1_::bool) = \
1.11 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.12 \ [Equation,fromFunction]) \
1.13 \ [bool_ (hd fs_), bool_ b1_]); \
1.14 -\ b2_ = Take (nth_ 2 rb_); \
1.15 +\ b2_ = nth_ 2 rb_; \
1.16 \ fs_ = filter (sameFunId (lhs b2_)) funs_; \
1.17 \ (e2_::bool) = \
1.18 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.19 \ [Equation,fromFunction]) \
1.20 \ [bool_ (hd fs_), bool_ b2_]) \
1.21 -\ b3_ = Take (nth_ 3 rb_); \
1.22 +\ b3_ = nth_ 3 rb_; \
1.23 \ fs_ = filter (sameFunId (lhs b3_)) funs_; \
1.24 \ (e3_::bool) = \
1.25 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.26 \ [Equation,fromFunction]) \
1.27 \ [bool_ (hd fs_), bool_ b3_]) \
1.28 -\ b4_ = Take (nth_ 4 rb_); \
1.29 +\ b4_ = nth_ 4 rb_; \
1.30 \ fs_ = filter (sameFunId (lhs b4_)) funs_; \
1.31 \ (e4_::bool) = \
1.32 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
2.1 --- a/src/sml/IsacKnowledge/Rational.ML Mon Sep 04 16:56:33 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Rational.ML Tue Sep 05 10:10:27 2006 +0200
2.3 @@ -598,7 +598,7 @@
2.4 (*. datatypes for internal representation.*)
2.5 type mv_monom = (int * (*.coefficient or the monom.*)
2.6 int list); (*.list of exponents) .*)
2.7 -fun mv_monom2str (i,is) = "("^int2str i^","^ints2str' is^")";
2.8 +fun mv_monom2str (i, is) = "("^ int2str i^"," ^ ints2str' is ^ ")";
2.9
2.10 type mv_poly = mv_monom list;
2.11 fun mv_poly2str p = (strs2str' o (map mv_monom2str)) p;
2.12 @@ -1558,31 +1558,23 @@
2.13 else Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
2.14 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
2.15 Free ((str_of_int o abs) i, HOLogic.realT)) $
2.16 - powerproduct2term(is, v);---------------------------*)
2.17 -fun monom2term ((i, is):mv_monom, v) =
2.18 + powerproduct2term(is, vs);---------------------------*)
2.19 +fun monom2term ((i, is) : mv_monom, vs) =
2.20 if allzeros is
2.21 then Free (str_of_int i, HOLogic.realT)
2.22 - else Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
2.23 - (Free (str_of_int i, HOLogic.realT)) $
2.24 - powerproduct2term(is, v);
2.25 + else if i = 1
2.26 + then powerproduct2term (is, vs)
2.27 + else Const ("op *", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
2.28 + (Free (str_of_int i, HOLogic.realT)) $
2.29 + powerproduct2term (is, vs);
2.30
2.31 -
2.32 -(*. converts the polynomial representation into the term representation .*)
2.33 -fun poly2term' ([]:mv_poly,vs) = Free(str_of_int 0,HOLogic.realT)
2.34 - | poly2term' ([(c,e)],vs) = monom2term((c,e),vs)
2.35 - | poly2term' ((c,e)::others,vs) = Const("op +",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
2.36 - poly2term(others,vs) $
2.37 - (
2.38 - monom2term((c,e),vs)
2.39 - )
2.40 -(*. translates the internal representation into an Isabelle term
2.41 - poly2term =
2.42 - fn : (int * (**)
2.43 - int list) list * (**)
2.44 - string list -> (**)
2.45 - term (**)
2.46 -.*)
2.47 -and poly2term (xs,vs) = poly2term'(rev(sort (mv_geq LEX_) (xs)),vs);
2.48 +(*. converts the internal polynomial representation into an Isabelle term.*)
2.49 +fun poly2term' ([] : mv_poly, vs) = Free(str_of_int 0, HOLogic.realT)
2.50 + | poly2term' ([(c, e) : mv_monom], vs) = monom2term ((c, e), vs)
2.51 + | poly2term' ((c, e) :: ces, vs) =
2.52 + Const("op +", [HOLogic.realT, HOLogic.realT] ---> HOLogic.realT) $
2.53 + poly2term (ces, vs) $ monom2term ((c, e), vs)
2.54 +and poly2term (xs, vs) = poly2term' (rev (sort (mv_geq LEX_) (xs)), vs);
2.55
2.56
2.57 (*. converts a monom into term representation .*)
3.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Mon Sep 04 16:56:33 2006 +0200
3.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Tue Sep 05 10:10:27 2006 +0200
3.3 @@ -694,34 +694,41 @@
3.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.7 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y 0 = 0";
3.8 -(*WN060902??? missing Substitute ???*)
3.9 -case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
3.10 +case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
3.11 | _ => raise error "biegelinie.sml: met setzeRandbed*Ein 1";
3.12 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.13 +(*
3.14 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.15 +(** upd_env_opt: (None,??.empty)
3.16 +*** upd_env_opt: (None,??.empty)
3.17 +*** upd_env_opt: (None,??.empty)
3.18 +*** upd_env_opt: (None,Subproblem (thy, [makeFunctionTo, equation]))
3.19 +*** upd_env_opt: (None,Subproblem (thy, [makeFunctionTo, equation]))
3.20 +*** upd_env_opt: (None,y 0 = 0)
3.21 +*** upd_env_opt: (None,y 0 = 0)
3.22 +*** upd_env_opt: (None,[y x = c_4 + c_3 * x + ...*)
3.23 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.24 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.25 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.26 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.27 +case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
3.28 +| _ => raise error "biegelinie.sml: met setzeRandbed*Ein 2";
3.29
3.30 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.31 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.32 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.33 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.34 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.35 - "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
3.36 + "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)" (*true*);
3.37 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.38 - "y 0 =\nc_4 + c_3 * 0 +\n1 / (-1 * EI) *\n(c_2 / 2 * 0 ^^^ 2 + c / 6 * 0 ^^^ 3 + -1 * q_0 / 24 * 0 ^^^ 4)";
3.39 + "y 0 =\nc_4 + c_3 * 0 +\n1 / (-1 * EI) *\n(c_2 / 2 * 0 ^^^ 2 + c / 6 * 0 ^^^ 3 + -1 * q_0 / 24 * 0 ^^^ 4)" (*true*);
3.40 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
3.41 - "0 =\nc_4 + c_3 * 0 +\n1 / (-1 * EI) *\n(c_2 / 2 * 0 ^^^ 2 + c / 6 * 0 ^^^ 3 + -1 * q_0 / 24 * 0 ^^^ 4)"
3.42 -;
3.43 + "0 =\nc_4 + c_3 * 0 +\n1 / (-1 * EI) *\n(c_2 / 2 * 0 ^^^ 2 + c / 6 * 0 ^^^ 3 + -1 * q_0 / 24 * 0 ^^^ 4)" (*true*);
3.44 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)";
3.45 (*WN060902 thm real_0_divide in rls reduce_0_1_2 in rls norm_Rational^^^notap*)
3.46 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)";
3.47 (*end of 1st "Randbedingung einsetzen"*)
3.48
3.49 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y L = 0";
3.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.51 (*WN060902 strange msgs also here !!!! GOON*)
3.52
3.53
3.54 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.55 -(*
3.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.57 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.58 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.59 @@ -863,6 +870,7 @@
3.60 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.61 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.62 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.63 +(********************************************* setzeRandbedingungenEin !!!!
3.64 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.65 case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"]) => ()
3.66 | _ => raise error "biegelinie.sml met2 e";
3.67 @@ -901,7 +909,7 @@
3.68 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.69 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.70 *)
3.71 -
3.72 +******************************************************************8*)
3.73
3.74 "----------- investigate normalforms -----------------------------";
3.75 "----------- investigate normalforms -----------------------------";
4.1 --- a/src/smltest/IsacKnowledge/rational.sml Mon Sep 04 16:56:33 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 10:10:27 2006 +0200
4.3 @@ -18,7 +18,10 @@
4.4 "-----------------------------------------------------------------";
4.5 "table of contents -----------------------------------------------";
4.6 "-----------------------------------------------------------------";
4.7 +"~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~~~~~~~~~~";
4.8 "-------- ... missing WN060103 -----------------------------------";
4.9 +"-------- fun monom2term, fun poly2term' ------------------------";
4.10 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
4.11 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
4.12 "-------- common_nominator_p ---------------------------- --------";
4.13 "-------- reverse rewrite ----------------------------------------";
4.14 @@ -40,18 +43,21 @@
4.15 "-----------------------------------------------------------------";
4.16
4.17
4.18 -(*. tests of internal functions: to make them work,
4.19 +"~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~~~~~~~~~~";
4.20 +(*.~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.21 + tests of internal functions: to make them work,
4.22 out-comment (*!!!*) in knowledge/Rational.ML:
4.23 -(*!!!
4.24 +(*##!!!
4.25 structure RationalI : RATIONALI =
4.26 struct
4.27 -!!!*)
4.28 +!!!##*)
4.29
4.30 -(*!!!
4.31 +(*##!!!
4.32 end;(*struct*)
4.33 open RationalI;
4.34 -!!!*)
4.35 +!!!##*)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~.*)
4.36
4.37 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.38 print("\n\n********************* rational.sml - TESTS *************************\n\n");
4.39 print("\n\n***** divide tests *****\n");
4.40 val mv_pquot1 = (#1(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
4.41 @@ -172,7 +178,29 @@
4.42 if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
4.43 val pp3=mv_pp [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
4.44
4.45 ----------------------------------------------------------------------------*)
4.46 +
4.47 +"-------- fun monom2term, fun poly2term' ------------------------";
4.48 +"-------- fun monom2term, fun poly2term' ------------------------";
4.49 +"-------- fun monom2term, fun poly2term' ------------------------";
4.50 +val t = monom2term ((3,[2,1,0]), ["c","b","a"](*reverse ???SK-*));
4.51 +term2str t = "3 * (c ^^^ 2 * b)" (*true*);
4.52 +
4.53 +val t = monom2term ((1,[1,0]), ["b","a"]);
4.54 +term2str t = "b" (*true*);
4.55 +
4.56 +val t = poly2term ([(1,[0,0,0]),(2,[1,0,0]),(3,[2,1,0]),(4,[3,2,1])],
4.57 + ["c","b","a"]);
4.58 +term2str t = "1 + 2 * c + 3 * (c ^^^ 2 * b) + 4 * (c ^^^ 3 * (b ^^^ 2 * a))";
4.59 +
4.60 +val t = poly2term ([(1,[1,0]),(1,[0,1])], ["b","a"]);
4.61 +term2str t = "a + b" (*true*);
4.62 +
4.63 +
4.64 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
4.65 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
4.66 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
4.67 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
4.68 +
4.69
4.70 fun parse_rat str = (term_of o the o (parse thy)) str;
4.71
4.72 @@ -380,10 +408,8 @@
4.73 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
4.74 val Some (t',_) = factout_ thy t;
4.75 val Some (t'',_) = cancel_ thy t;
4.76 -term2str t'= "(1 * y + x) * (1 * y - x) / ((1 * y - x) * (1 * y - x))"(*true*);
4.77 -(*sometime before 060831???SK..*)"(y + x) * (y - x) / ((y - x) * (y - x))";
4.78 -term2str t'' = "(1 * y + x) / (1 * y - x)" (*true*);
4.79 -(*sometime before 060831???SK1..*)"(y + x) / (y - x)";
4.80 +term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*);
4.81 +term2str t'' = "(y + x) / (y - x)";
4.82
4.83 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
4.84 val Some (t',_) = common_nominator_ thy t;
4.85 @@ -391,11 +417,7 @@
4.86 term2str t' =
4.87 "(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1\
4.88 \ * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*);
4.89 -term2str t'' = "(-1 - x - y) / (1 * x - y)" (*true*);
4.90 -(*sometime before 060831???SK2..*)
4.91 -"((-1) * x ^^^ 2 + y ^^^ 2) / (((-1) * x + y) * ((-1) * x + y)) +\
4.92 -\1 * ((-1) * x + y) / (((-1) * x + y) * ((-1) * x + y))";
4.93 -(*sometime before 060831???SK2..*)"((-1) - x - y) / (x - y)";
4.94 +term2str t'' = "(-1 - x - y) / (x - y)" (*true*);
4.95
4.96 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
4.97 val Some (t',_) = common_nominator_ thy t;
4.98 @@ -403,12 +425,8 @@
4.99 term2str t' =
4.100 "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x)) +\n1\
4.101 \ * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" (*true*);
4.102 -term2str t'' = "(-1 - y - x) / (1 * y - x)" (*true*);
4.103 -(*sometime before 060831???SK3..*)
4.104 -"((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
4.105 -\1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
4.106 -(*sometime before 060831???SK3..*)"((-1) - y - x) / (y - x)";
4.107 -(*WN.16.10.02 lexicographische Ordnung ^^^^^^^ ?!*)
4.108 +term2str t'' = "(-1 - y - x) / (y - x)" (*true*);
4.109 +(*WN.16.10.02 lexicographische ^^^^^^^ Ordnung ???SK-*)
4.110
4.111
4.112 val t=(term_of o the o (parse thy))
4.113 @@ -906,7 +924,7 @@
4.114
4.115 (*initialize the interpreter state used by the 'me'*)
4.116 val Some (t', asm) = cancel_p_ thy t;
4.117 -term2str t' = "(3 + 1 * x) / (3 + -1 * x)" (*true*);
4.118 +term2str t' = "(3 + x) / (3 + -1 * x)" (*true*);
4.119 terms2str asm = "[\"3 + -1 * x ~= 0\"]" (*true*);
4.120 val (t,_,revsets,_) = ini t;
4.121
4.122 @@ -1995,16 +2013,17 @@
4.123 interSteps 1 ([1,2,1],Res);
4.124 val ((pt,p),_) = get_calc 1; show_pt pt;
4.125 val newnds = children (get_nd pt [1,2,1]) (*see "fun detailrls"*);
4.126 -if length newnds = 12 then ()
4.127 +(*if length newnds = 12 then () WN060905*)
4.128 +if length newnds = 13 then ()
4.129 else raise error "rational.sml: interSteps cancel_p rev_rew_p";
4.130
4.131 val p = ([1,2,1,9],Res);
4.132 getTactic 1 p;
4.133 val (_, tac, _) = pt_extract (pt, p);
4.134 -if tac =
4.135 - Some (Rewrite("sym_real_plus_binom_times1",
4.136 - "?a ^^^ 2 + -1 * ?b ^^^ 2 = (?a + 1 * ?b) * (?a + -1 * ?b)"))
4.137 -then () else raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
4.138 +(*case tac of Some (Rewrite ("sym_real_plus_binom_times1", _)) => ()
4.139 +WN060905*)
4.140 +case tac of Some (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
4.141 +| _ => raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
4.142
4.143
4.144 "-------- investigate rulesets for cancel_p ----------------------";
4.145 @@ -2075,12 +2094,12 @@
4.146 "----- see Rational.ML, local cancel_p, fun init_state";
4.147 val t = str2term "a^^^2 / a";
4.148 val Some (t',_) = factout_p_ thy t;
4.149 -term2str t' = "1 * a * (1 * a) / (1 * (1 * a))" (*true*);
4.150 +term2str t' = "a * a / (1 * a)" (*true*);
4.151 (*... can be canceled with
4.152 real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
4.153 (* sml/ME/rewtools.sml:
4.154 val rtas = reverse_deriv thy Atools_erls rules ro None t';
4.155 -writeln(deri2str rtas);
4.156 +writeln (deri2str rtas);
4.157 *)
4.158
4.159
4.160 @@ -2117,7 +2136,7 @@
4.161 (* cancel_p_ thy t;
4.162 Warning - Increasing stack from 147456 to 294912 bytes
4.163 Warning - Increasing stack from 294912 to 589824 bytes
4.164 - Warning - Increasing stack from 589824 to 1179648 bytes)
4.165 + Warning - Increasing stack from 589824 to 1179648 bytes*)
4.166
4.167
4.168 "----- SK060904-2a non-termination of add_fraction_p_";
5.1 --- a/src/smltest/IsacKnowledge/rlang.sml Mon Sep 04 16:56:33 2006 +0200
5.2 +++ b/src/smltest/IsacKnowledge/rlang.sml Tue Sep 05 10:10:27 2006 +0200
5.3 @@ -1,4 +1,5 @@
5.4 (* use"../smltest/IsacKnowledge/rlang.sml";
5.5 + use"rlang.sml";
5.6 *)
5.7
5.8 (******************************************************************
5.9 @@ -1411,7 +1412,7 @@
5.10 Nundef,
5.11 "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 * d ^^^ 2 / d ^^^ 2 +\n-4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 =\n0")) then ()*)
5.12 if f2str f =
5.13 - "c ^^^ 4 / d ^^^ 2 + 1 * A ^^^ 2 / 1 + -4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 = 0"
5.14 + "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 / 1 + -4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 = 0"
5.15 then () else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a";
5.16 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.17 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;