Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/algein.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37991 028442673981
child 38050 4c52ad406c20
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba 
    86 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
 
    86 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
 
    87 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
 
    87 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
 
    88 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
 
    88 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
 
    89 val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
 
    89 val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
 
    90 if f2str f = "L = 32 + senkrecht + unten" then ()
 
    90 if f2str f = "L = 32 + senkrecht + unten" then ()
 
    91 else raise error "algein.sml diff.behav. in erstSymbolisch 1";
 
    91 else error "algein.sml diff.behav. in erstSymbolisch 1";
 
    92 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    92 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    93 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    93 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    94 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    94 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    95 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    95 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
 
    96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
    97 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
 
    97 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
 
    98 else raise error "algein.sml diff.behav. in erstSymbolisch 99";
 
    98 else error "algein.sml diff.behav. in erstSymbolisch 99";
 
    99 
    99 
   100 
   100 
   101 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 
   101 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 
   102 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 
   102 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 
   103 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 
   103 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
 
   113 Iterator 1;
 
   113 Iterator 1;
 
   114 moveActiveRoot 1;
 
   114 moveActiveRoot 1;
 
   115 autoCalculate 1 CompleteCalc;
 
   115 autoCalculate 1 CompleteCalc;
 
   116 val ((pt,p),_) = get_calc 1; show_pt pt;
 
   116 val ((pt,p),_) = get_calc 1; show_pt pt;
 
   117 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
 
   117 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
 
   118 else raise error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
 
   118 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
 
   119 
   119 
   120 (*
 
   120 (*
 
   121 show_pt pt;
 
   121 show_pt pt;
 
   122 trace_rewrite:=true;
 
   122 trace_rewrite:=true;
 
   123 trace_rewrite:=false;
 
   123 trace_rewrite:=false;
wneuper/isa