1.1 --- a/test/Tools/isac/IsacKnowledge/biegelinie.sml Tue Aug 17 09:05:51 2010 +0200
1.2 +++ b/test/Tools/isac/IsacKnowledge/biegelinie.sml Wed Aug 18 13:40:09 2010 +0200
1.3 @@ -30,20 +30,20 @@
1.4 "----------- the rules -------------------------------------------";
1.5 "----------- the rules -------------------------------------------";
1.6 "----------- the rules -------------------------------------------";
1.7 -fun str2t str = (term_of o the o (parse Biegelinie.thy)) str;
1.8 +fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
1.9 fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
1.10 fun rewrit thm str =
1.11 fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
1.12
1.13 -val t = rewrit Belastung_Querkraft (str2t "- q_ x = - q_0"); term2s t;
1.14 +val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
1.15 if term2s t = "Q' x = - q_0" then ()
1.16 else raise error "/biegelinie.sml: Belastung_Querkraft";
1.17
1.18 -val t = rewrit Querkraft_Moment (str2t "Q x = - q_0 * x + c"); term2s t;
1.19 +val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t;
1.20 if term2s t = "M_b' x = - q_0 * x + c" then ()
1.21 else raise error "/biegelinie.sml: Querkraft_Moment";
1.22
1.23 -val t = rewrit Moment_Neigung (str2t "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.24 +val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
1.25 term2s t;
1.26 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
1.27 else raise error "biegelinie.sml: Moment_Neigung";
1.28 @@ -125,7 +125,7 @@
1.29 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.30 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.31 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
1.32 -val t = str2t "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
1.33 +val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
1.34 val t = rewrit Moment_Neigung t; term2s t;
1.35 (*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
1.36 ### before declaring "y''" as a constant *)
1.37 @@ -191,18 +191,18 @@
1.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.39 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.40
1.41 -val pits = get_obj g_pbl pt (fst p);writeln (itms2str thy pits);
1.42 -(*if itms2str thy pits = ... all 5 model-items*)
1.43 -val mits = get_obj g_met pt (fst p); writeln (itms2str thy mits);
1.44 -if itms2str thy mits = "[]" then ()
1.45 +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
1.46 +(*if itms2str_ ctxt pits = ... all 5 model-items*)
1.47 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
1.48 +if itms2str_ ctxt mits = "[]" then ()
1.49 else raise error "biegelinie.sml: Bsp 7.27 #2";
1.50
1.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.52 case nxt of (_,Add_Given "FunktionsVariable x") => ()
1.53 | _ => raise error "biegelinie.sml: Bsp 7.27 #4a";
1.54 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.55 -val mits = get_obj g_met pt (fst p);writeln (itms2str thy mits);
1.56 -(*if itms2str thy mits = ... all 6 guard-items*)
1.57 +val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
1.58 +(*if itms2str_ ctxt mits = ... all 6 guard-items*)
1.59 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.60 | _ => raise error "biegelinie.sml: Bsp 7.27 #4b";
1.61