test/Tools/isac/IsacKnowledge/biegelinie.sml
branchisac-update-Isa09-2
changeset 37924 6c53fe2519e5
parent 37906 e2b23ba9df13
child 37926 e6fc98fbcb85
     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