1.1 --- a/src/sml/ME/generate.sml Sat Mar 05 18:08:56 2005 +0100
1.2 +++ b/src/sml/ME/generate.sml Sat Mar 05 18:08:56 2005 +0100
1.3 @@ -240,13 +240,13 @@
1.4 end
1.5
1.6 | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt =
1.7 - (writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
1.8 + ((*writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
1.9 writeln("###generate1 Apply_Method': topt= "^termopt2str topt);
1.10 - writeln("###generate1 Apply_Method': is = "^istate2str is);
1.11 + writeln("###generate1 Apply_Method': is = "^istate2str is);*)
1.12 case topt of
1.13 Some t =>
1.14 let val (pt,_) = cappend_form pt p is t
1.15 - val _= writeln("###generate1 Apply_Method: after cappend")
1.16 + (*val _= writeln("###generate1 Apply_Method: after cappend")*)
1.17 in (pos,[(*WN0502: pblnd generated without children*)], EmptyMout,pt)
1.18 end
1.19 | None =>
1.20 @@ -281,7 +281,7 @@
1.21 pt) end
1.22
1.23 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
1.24 - let val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));
1.25 + let (*val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
1.26 val (pt,c) = cappend_atomic pt p l f
1.27 (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
1.28 val pt = update_branch pt p TransitiveB (*040312*)
1.29 @@ -290,7 +290,7 @@
1.30 pt) end
1.31
1.32 | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
1.33 - let val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))
1.34 + let (*val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
1.35 val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
1.36 val pt = update_branch pt p TransitiveB (*040312*)
1.37 (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.38 @@ -304,7 +304,7 @@
1.39 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
1.40 (assoc_thy "Isac.thy", tac_, is, pos, pt);
1.41 *)
1.42 - let val _= writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str (p,p_))
1.43 + let (*val _=writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
1.44 val (pt,c) = cappend_atomic pt p l f
1.45 (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
1.46 val pt = update_branch pt p TransitiveB (*040312*)
1.47 @@ -322,7 +322,7 @@
1.48 in (*implicit Take*) generate1 thy tac_ is pos' pt end
1.49
1.50 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
1.51 - let val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))
1.52 + let (*val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
1.53 val (pt,c) = cappend_atomic pt p l f
1.54 (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.55 val pt = update_branch pt p TransitiveB (*040312*)
1.56 @@ -340,7 +340,7 @@
1.57 in (*implicit Take*) generate1 thy tac_ is pos' pt end
1.58
1.59 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
1.60 - let val _= writeln("###generate1 Check_Postcond': pos= "^pos'2str (p,p_))
1.61 + let (*val _=writeln("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
1.62 (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
1.63 val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
1.64 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
1.65 @@ -352,7 +352,7 @@
1.66 pt)end
1.67
1.68 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
1.69 - let val _=writeln("###generate1 Check_elementwise': pos= "^pos'2str (p,p_))
1.70 + let(*val _=writeln("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*)
1.71 val (pt,c) = cappend_atomic pt p l consts
1.72 (Check_elementwise pred) (f',asm) Complete;
1.73 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.74 @@ -371,7 +371,7 @@
1.75
1.76 | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f))
1.77 l (p,p_) pt =
1.78 - let val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))
1.79 + let (*val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
1.80 val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
1.81 (oris, (domID, pblID, metID), hdl);
1.82 (*val pbl = init_pbl ((#ppc o get_pbt) pblID);
1.83 @@ -394,7 +394,7 @@
1.84
1.85 (*tacis are in reverse order from nxt_solve_/specify_: last = hd*)
1.86 fun generate ([]: taci list) ptp =
1.87 - (writeln("### generate END-------------------------------");
1.88 + (writeln("### generate END (no matching pattern found)-------------");
1.89 ptp)
1.90 (* val (tacis, (pt, _)) = (tacis, ptp);
1.91 *)
1.92 @@ -403,7 +403,7 @@
1.93 val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt
1.94 in generate tacis' (pt', c@c', p') end;
1.95
1.96 -
1.97 +
1.98
1.99 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
1.100 * of for connecting a user-input formula with the current calc-state. *
2.1 --- a/src/sml/ROOT.ML Sat Mar 05 18:08:56 2005 +0100
2.2 +++ b/src/sml/ROOT.ML Sat Mar 05 18:08:56 2005 +0100
2.3 @@ -72,9 +72,9 @@
2.4 ############## unten: (*systest/ctree.sml*) wegen cut_tree in ME/ctree !!!
2.5 *)
2.6
2.7 - val version_kernel = "sml-050217a-fetchApplicableTactics";
2.8 + val version_kernel = "sml-050305d-cut_tree";
2.9
2.10 - print_depth 3;
2.11 + print_depth 3;
2.12
2.13 (*----- Isabelle2003/src/Pure/library.ML overwritten by later Isa-code*)
2.14 fun find_first _ [] = None