1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Thu Jul 21 12:01:56 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Fri Jul 22 14:01:09 2011 +0200
     1.3 @@ -17,8 +17,7 @@
     1.4  "-----------------------------------------------------------------";
     1.5  "-----------------------------------------------------------------";
     1.6  
     1.7 -(*=== inhibit exn ?=============================================================
     1.8 -val thy = AlgEin.thy;
     1.9 +val thy = @{theory "AlgEin"};
    1.10  
    1.11  
    1.12  (* use"../smltest/IsacKnowledge/algein.sml";
    1.13 @@ -33,8 +32,10 @@
    1.14  \ (let t_ = (l_ = 1)\
    1.15  \ in t_)"
    1.16  ;
    1.17 +(*=== inhibit exn 110722=============================================================
    1.18  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.19 -(*---^^^-OK-----------------------------------------------------------------*)
    1.20 +=== inhibit exn 110722=============================================================*)
    1.21 +
    1.22  val str =
    1.23  "Script RechnenSymbolScript (k_::bool) (q__::bool)           \
    1.24  \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
    1.25 @@ -46,14 +47,12 @@
    1.26  \      t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
    1.27  \ in t_)"
    1.28  ;
    1.29 +(*=== inhibit exn 110722=============================================================
    1.30  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.31 -(*---vvv-NOTok--------------------------------------------------------------*)
    1.32 -
    1.33 -
    1.34  
    1.35  atomty sc;
    1.36  atomt sc;
    1.37 -
    1.38 +=== inhibit exn 110722=============================================================*)
    1.39  
    1.40  "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
    1.41  "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
    1.42 @@ -68,6 +67,7 @@
    1.43    ("Isac",["numerischSymbolische", "Berechnung"],
    1.44     ["Berechnung","erstNumerisch"]);
    1.45  val p = e_pos'; val c = [];
    1.46 +(*=== inhibit exn 110722=============================================================
    1.47  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
    1.48  val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
    1.49  val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
    1.50 @@ -97,12 +97,12 @@
    1.51  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.52  if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
    1.53  else error "algein.sml diff.behav. in erstSymbolisch 99";
    1.54 -
    1.55 + DEconstrCalcTree 1;
    1.56 +=== inhibit exn 110722=============================================================*)
    1.57  
    1.58  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
    1.59  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
    1.60  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
    1.61 -states:=[];
    1.62  CalcTree
    1.63  [(["KantenLaenge (k=10)","Querschnitt (q=1)",
    1.64     "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", 
    1.65 @@ -115,9 +115,10 @@
    1.66  moveActiveRoot 1;
    1.67  autoCalculate 1 CompleteCalc;
    1.68  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.69 +(*=== inhibit exn 110722=============================================================
    1.70  if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
    1.71  else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
    1.72 -
    1.73 +===== inhibit exn 110722===========================================================*)
    1.74  (*
    1.75  show_pt pt;
    1.76  trace_rewrite:=true;
    1.77 @@ -125,14 +126,13 @@
    1.78  trace_script:=true;
    1.79  trace_script:=false;
    1.80  *)
    1.81 -
    1.82  "----------- Widerspruch 3 = 777 ---------------------------------";
    1.83  "----------- Widerspruch 3 = 777 ---------------------------------";
    1.84  "----------- Widerspruch 3 = 777 ---------------------------------";
    1.85 -val thy = (theory "Isac"); 
    1.86 +val thy = @{theory "Isac"}; 
    1.87  val rew_ord = dummy_ord;
    1.88  val erls = Erls;
    1.89 -
    1.90 +(*===== inhibit exn 110722===========================================================
    1.91  val thm = assoc_thm' thy ("sym_real_mult_0_right","");
    1.92  val t = str2term "0 = 0";
    1.93  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
    1.94 @@ -148,6 +148,7 @@
    1.95  val t'' = subst_atomic subst t';
    1.96  term2str t'';
    1.97  (********"0 = 3 * 0"*)
    1.98 +===== inhibit exn 110722===========================================================*)
    1.99  
   1.100  val thm = assoc_thm' thy ("sym","");
   1.101  (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
   1.102 @@ -157,4 +158,3 @@
   1.103  (* use"../smltest/IsacKnowledge/algein.sml";
   1.104     *)
   1.105  
   1.106 -===== inhibit exn ?===========================================================*)