1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Jan 05 17:43:48 2012 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sat Jan 07 10:06:06 2012 +0100
     1.3 @@ -549,44 +549,33 @@
     1.4    (2) Pattern.match: for solving equational systems 
     1.5        (which raises exn for ?a..?z)*)
     1.6    | applicable_in (p,p_) pt (m as Substitute sube) = 
     1.7 -  if member op = [Pbl,Met] p_ 
     1.8 -  then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
     1.9 -  else let val pp = par_pblobj pt p
    1.10 -	   val thy = assoc_thy (get_obj g_domID pt pp)
    1.11 -	   val f = case p_ of
    1.12 -		       Frm => get_obj g_form pt p
    1.13 -		     | Res => (fst o (get_obj g_result pt)) p
    1.14 -	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    1.15 -	   val subte = sube2subte sube
    1.16 -	   val subst = sube2subst thy sube
    1.17 -       in if foldl and_ (true, map contains_Var subte)
    1.18 -	  (*1*)
    1.19 -	  then let val f' = subst_atomic subst f
    1.20 -	       in if f = f' then Notappl (sube2str sube^" not applicable")
    1.21 -		  else Appl (Substitute' (subte, f, f'))
    1.22 -	       end
    1.23 -	  (*2*)
    1.24 -	  else case rewrite_terms_ thy (assoc_rew_ord rew_ord') 
    1.25 -				   erls subte f of
    1.26 -		   SOME (f', _) =>  Appl (Substitute' (subte, f, f'))
    1.27 -		 | NONE => Notappl (sube2str sube^" not applicable")
    1.28 -       end
    1.29 -(*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
    1.30 -  | applicable_in (p,p_) pt (m as Substitute sube) = 
    1.31 -  if member op = [Pbl,Met] p_ 
    1.32 -  then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.33 -  else let val pp = par_pblobj pt p
    1.34 -	   val thy = assoc_thy (get_obj g_domID pt pp)
    1.35 -	   val f = case p_ of
    1.36 -		       Frm => get_obj g_form pt p
    1.37 -		     | Res => (fst o (get_obj g_result pt)) p
    1.38 -	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    1.39 -	   val subte = sube2subte sube
    1.40 -       in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
    1.41 -	      SOME (f', _) =>  Appl (Substitute' (subte, f, f'))
    1.42 -	    | NONE => Notappl (sube2str sube^" not applicable")
    1.43 -       end
    1.44 -------------------*)
    1.45 +      if member op = [Pbl,Met] p_ 
    1.46 +      then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.47 +      else 
    1.48 +        let
    1.49 +          val pp = par_pblobj pt p
    1.50 +          val thy = assoc_thy (get_obj g_domID pt pp)
    1.51 +          val f = case p_ of
    1.52 +		        Frm => get_obj g_form pt p
    1.53 +		      | Res => (fst o (get_obj g_result pt)) p
    1.54 +		      val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    1.55 +		      val subte = sube2subte sube
    1.56 +		      val subst = sube2subst thy sube
    1.57 +		      val ro = assoc_rew_ord rew_ord'
    1.58 +		    in
    1.59 +		      if foldl and_ (true, map contains_Var subte)
    1.60 +		      (*1*)
    1.61 +		      then
    1.62 +		        let val f' = subst_atomic subst f
    1.63 +		        in if f = f' then Notappl (sube2str sube^" not applicable")
    1.64 +		           else Appl (Substitute' (ro, erls, subte, f, f'))
    1.65 +		        end
    1.66 +		        (*2*)
    1.67 +		      else 
    1.68 +		        case rewrite_terms_ thy ro erls subte f of
    1.69 +		            SOME (f', _) =>  Appl (Substitute' (ro, erls, subte, f, f'))
    1.70 +		          | NONE => Notappl (sube2str sube^" not applicable")
    1.71 +		    end
    1.72  
    1.73    | applicable_in p pt (Apply_Assumption cts') = 
    1.74        (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts'))))

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Thu Jan 05 17:43:48 2012 +0100
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Sat Jan 07 10:06:06 2012 +0100
     2.3 @@ -223,27 +223,16 @@
     2.4  val e_subte = []:term list;
     2.5  fun subte2str ss = terms2str ss;
     2.6  
     2.7 -fun subte2sube ss = map term2str ss;
     2.8 -
     2.9 -fun subst2subs s = map (pair2str o (apfst term2str) o (apsnd term2str)) s;
    2.10 -fun subst2subs' s = map ((apfst term2str) o (apsnd term2str)) s;
    2.11 +val subte2sube = map term2str;
    2.12 +val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
    2.13 +val subst2subs' = map ((apfst term2str) o (apsnd term2str));
    2.14  fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
    2.15 -(*> subs2subst thy ["(bdv,x)","(err,#0)"];
    2.16 -val it =
    2.17 -  [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
    2.18 -   (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))] 
    2.19 -   : (term * term) list*)
    2.20 -(*["bdv=x","err=0"] ---> [(bdv,x), (err,0)]*)
    2.21  fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;
    2.22 -(* val ts = sube2subst thy ["bdv=x","err=0"];
    2.23 -   subst2str' ts;
    2.24 -   *)
    2.25 -fun sube2subte ss = map str2term ss;
    2.26 -
    2.27 +val sube2subte = map str2term;
    2.28 +val subte2subst = map HOLogic.dest_eq;
    2.29  
    2.30  fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
    2.31  
    2.32 -
    2.33  type scrstate =       (*state for script interpreter*)
    2.34  	 env(*stack*) (*used to instantiate tac for checking assod
    2.35  		       12.03.noticed: e_ not updated during execution ?!?*)
    2.36 @@ -255,6 +244,11 @@
    2.37  	 * bool;      (*true = strongly .., false = weakly associated: 
    2.38  					    only used during ass_dn/up*)
    2.39  val e_scrstate = ([],[],NONE,e_term,Sundef,false):scrstate;
    2.40 +fun topt2str NONE = "NONE"
    2.41 +  | topt2str (SOME t) = "SOME" ^ term2str t;
    2.42 +fun scrstate2str (env, loc_, topt, t, safe, bool) =
    2.43 +  "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^ 
    2.44 +  term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
    2.45  
    2.46  (* for handling type istate see fun from_pblobj_or_detail', +? *)
    2.47  datatype istate =           (*interpreter state*)
    2.48 @@ -520,8 +514,16 @@
    2.49  type fmz = fmz_ * spec;
    2.50  val e_fmz = ([],e_spec);
    2.51  
    2.52 -(* tac_ is made from tac in applicable_in,
    2.53 -  and carries all data necessary for generate *)
    2.54 +(* tac_ contains results from check in 'fun applicable_in'.
    2.55 +  This is useful for costly results, e.g. from rewriting;
    2.56 +  however, these results might be changed by Scripts like
    2.57 +      "      eq = (Rewrite_Set ansatz_rls False) eql;" ^
    2.58 +      "      eq = drop_questionmarks eq;" ^
    2.59 +      "      eq = (Rewrite_Set equival_trans False) eq;" ^
    2.60 +  WN120106 TODO ANALOGOUSLY TO Substitute':
    2.61 +  So tac_ contains the term t the result was calculated from
    2.62 +  in order to compare t with t' possibly changed by "Expr "
    2.63 +  and re-calculate result if t<>t'*)
    2.64  datatype tac_ = 
    2.65      Init_Proof' of ((cterm' list) * spec)
    2.66    | Model_Problem' of
    2.67 @@ -576,9 +578,11 @@
    2.68    | Derive' of rls
    2.69    | Calculate' of theory' * string * term * (term * thm') 
    2.70    | Substitute' of
    2.71 -      subte *   (*the 'substitution': terms of type bool*) 
    2.72 -		  term * (*to be substituted in*)
    2.73 -		  term (*resulting from the substitution*)
    2.74 +      rew_ord_ * (*for re-calculation                    *)
    2.75 +      rls *      (*for re-calculation                    *)
    2.76 +      subte *    (*the 'substitution': terms of type bool*) 
    2.77 +		  term * (*to be substituted in                  *)
    2.78 +		  term   (*resulting from the substitution       *)
    2.79    | Apply_Assumption' of term list * term
    2.80    | Take' of term
    2.81    | Take_Inst' of term  
    2.82 @@ -665,7 +669,7 @@
    2.83  
    2.84    | Derive' rls              => "Derive' "^id_rls rls
    2.85    | Calculate'  _            => "Calculate' "
    2.86 -  | Substitute' subs         => "Substitute' "(*^(subs2str subs)*)    
    2.87 +  | Substitute' _            => "Substitute' "(*^(subs2str subs)*)    
    2.88    | Apply_Assumption' ct's   => "Apply_Assumption' "(*^(strs2str ct's)*)
    2.89  
    2.90    | Take' cterm'             => "Take' "(*^(quote cterm'	)*)

     3.1 --- a/src/Tools/isac/Interpret/generate.sml	Thu Jan 05 17:43:48 2012 +0100
     3.2 +++ b/src/Tools/isac/Interpret/generate.sml	Sat Jan 07 10:06:06 2012 +0100
     3.3 @@ -464,7 +464,7 @@
     3.4    in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)),
     3.5        pt) end
     3.6  
     3.7 -  | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt =
     3.8 +  | generate1 thy (Substitute' (_, _, subte, t, t')) l (p,p_) pt =
     3.9        let 
    3.10          val (pt,c) =
    3.11            cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;

     4.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Jan 05 17:43:48 2012 +0100
     4.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat Jan 07 10:06:06 2012 +0100
     4.3 @@ -468,17 +468,21 @@
     4.4    	  term     (*for itr_arg,result in ets*)
     4.5    | NotAss;
     4.6  
     4.7 -(*.assod: tac_ associated with stac w.r.t. d
     4.8 +(* check if tac_ is associated with stac.
     4.9 +   Additional task: check if term t (the result has been calculated from) in tac_
    4.10 +   has been changed (see "datatype tac_"); if yes, recalculate result
    4.11 +   TODO.WN120106 recalculate impl.only for Substitute'
    4.12  args
    4.13 - pt:ptree for pushing the thy specified in rootpbl into subpbls
    4.14 +  pt     : ptree for pushing the thy specified in rootpbl into subpbls
    4.15 +  d      : unused (planned for data for comparison)
    4.16 +  tac_   : from user (via applicable_in); to be compared with ...
    4.17 +  stac   : found in Script
    4.18  returns
    4.19 - Ass    : associated: e.g. thmID in stac = thmID in m
    4.20 +  Ass    : associated: e.g. thmID in stac = thmID in m
    4.21                         +++ arg   in stac = arg   in m
    4.22 - AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
    4.23 - NotAss :             e.g. thmID in stac/=/thmID in m (not =)
    4.24 -8.01:
    4.25 - tac_ SubProblem with args completed from script
    4.26 -.*)
    4.27 +  AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
    4.28 +  NotAss :             e.g. thmID in stac/=/thmID in m (not =)
    4.29 +*)
    4.30  fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =
    4.31        (case stac of
    4.32  	       (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
    4.33 @@ -579,8 +583,18 @@
    4.34    | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) =
    4.35  	    Ass (m, term)
    4.36  
    4.37 -  | assod pt _ (m as Substitute' (_, _, res)) (Const ("Script.Substitute",_) $ _ $ _) =
    4.38 -	    Ass (m, res) 
    4.39 +  | assod pt _ (m as Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute",_) $ _ $ t) =
    4.40 +	    if f = t then Ass (m, f')
    4.41 +	    else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
    4.42 +		    if foldl and_ (true, map contains_Var subte)
    4.43 +		    then
    4.44 +		      let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
    4.45 +		      in if t = t' then error "assod: Substitute' not applicable to val of Expr"
    4.46 +		         else Ass (Substitute' (ro, erls, subte, t, t'), t')
    4.47 +		      end
    4.48 +		    else (case rewrite_terms_ (Isac()) ro erls subte t of
    4.49 +		         SOME (t', _) =>  Ass (Substitute' (ro, erls, subte, t, t'), t')
    4.50 +		       | NONE => error "assod: Substitute' not applicable to val of Expr")
    4.51  
    4.52    | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
    4.53        if id = id'
    4.54 @@ -664,7 +678,7 @@
    4.55  
    4.56    | tac_2tac (Or_to_List' _) = Or_to_List
    4.57    | tac_2tac (Take' term) = Take (term2str term)
    4.58 -  | tac_2tac (Substitute' (subte, t, res)) = Substitute (subte2sube subte) 
    4.59 +  | tac_2tac (Substitute' (_, _, subte, t, res)) = Substitute (subte2sube subte) 
    4.60  
    4.61    | tac_2tac (Tac_ (_,f,id,f')) = Tac id
    4.62  
    4.63 @@ -829,7 +843,7 @@
    4.64    | rep_tac_ (Check_elementwise' (t,str,(t',asm)))  = (Erule, (e_term, t'))
    4.65    | rep_tac_ (Subproblem' (_, _, _, _, _, t'))  = (Erule, (e_term, t'))
    4.66    | rep_tac_ (Take' (t'))  = (Erule, (e_term, t'))
    4.67 -  | rep_tac_ (Substitute' (subst,t,t'))  = (Erule, (t, t'))
    4.68 +  | rep_tac_ (Substitute' (_, _, subst,t,t'))  = (Erule, (t, t'))
    4.69    | rep_tac_ (Or_to_List' (t, t'))  = (Erule, (t, t'))
    4.70    | rep_tac_ m = error ("rep_tac_: not impl.for "^
    4.71  				 (tac_2str m));
    4.72 @@ -843,9 +857,9 @@
    4.73  
    4.74  
    4.75  (* handle a leaf at the end of recursive descent:
    4.76 -   a leaf is either a tactic or an 'exp' in 'let v = expr'
    4.77 -   where 'exp' does not contain a tactic.
    4.78 -   handling a leaf comprises
    4.79 +   a leaf is either a tactic or an 'expr' in "let v = expr"
    4.80 +   where "expr" does not contain a tactic.
    4.81 +   Handling a leaf comprises
    4.82     (1) 'subst_stacexpr' substitute env and complete curried tactic
    4.83     (2) rewrite the leaf by 'srls'
    4.84  *)
    4.85 @@ -854,7 +868,7 @@
    4.86         case subst_stacexpr E a v t of
    4.87  	       (a', STac stac) => (*script-tactic*)
    4.88  	         let val stac' =
    4.89 -             eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
    4.90 +               eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
    4.91  	         in
    4.92               (if (!trace_script) 
    4.93  	            then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'")
    4.94 @@ -863,12 +877,12 @@
    4.95  	         end
    4.96         | (a', Expr lexpr) => (*leaf-expression*)
    4.97  	         let val lexpr' =
    4.98 -             eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
    4.99 +               eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
   4.100  	         in
   4.101               (if (!trace_script) 
   4.102  	            then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
   4.103  	            else ();
   4.104 -	            (a', Expr lexpr'))
   4.105 +	            (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
   4.106  	         end;
   4.107  
   4.108  
   4.109 @@ -917,7 +931,7 @@
   4.110               val id' = mk_Free (id, T);
   4.111  	           val E' = upd_env E' (id', v);
   4.112  	         in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
   4.113 -       | NasNap (v,E) => 	 
   4.114 +       | NasNap (v,E) =>
   4.115  	         let
   4.116               val id' = mk_Free (id, T);
   4.117  	           val E' = upd_env E (id', v);
   4.118 @@ -983,7 +997,7 @@
   4.119        (case handle_leaf "locate" thy' sr E a v t of
   4.120  	       (a', Expr s) => 
   4.121  	          (NasNap (eval_listexpr_ (assoc_thy thy') sr
   4.122 -			         (subst_atomic (upd_env_opt E (a',v)) t), E))
   4.123 +			     (subst_atomic (upd_env_opt E (a',v)) t), E))
   4.124         | (a', STac stac) =>
   4.125  	         let
   4.126               val p' = 
   4.127 @@ -994,7 +1008,7 @@
   4.128               case assod pt d m stac of
   4.129  	             Ass (m,v') =>
   4.130  	               let val (p'',c',f',pt') =
   4.131 -                   generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
   4.132 +                     generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
   4.133  	               in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
   4.134               | AssWeak (m,v') => 
   4.135  	               let val (p'',c',f',pt') =
   4.136 @@ -1210,11 +1224,12 @@
   4.137  			         (last_elem o fst) p = 0 andalso snd p = Res)
   4.138  	           then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
   4.139  	           else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
   4.140 -	        Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
   4.141 -	          (if bb
   4.142 -             then Steps (ScrState is, ss)
   4.143 -	           else
   4.144 -               if rew_only ss (*andalso 'not bb'= associated weakly*)
   4.145 +	        Assoc (iss as (is as (_,_,_,_,_,strong_ass), ss as ((m',f',pt',p',c')::_))) =>
   4.146 +	          (if strong_ass
   4.147 +             then
   4.148 +              (Steps (ScrState is, ss))
   4.149 +	         else
   4.150 +               if rew_only ss (*andalso 'not strong_ass'= associated weakly*)
   4.151  	             then
   4.152                   let
   4.153                     val (po,p_) = p

     5.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Thu Jan 05 17:43:48 2012 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sat Jan 07 10:06:06 2012 +0100
     5.3 @@ -114,19 +114,17 @@
     5.4    ]);
     5.5  *}
     5.6  
     5.7 -
     5.8 -
     5.9  text {* this definition's scope is all Isac; so no equation etc with "A" would be possible:
    5.10  consts
    5.11    A :: "real"
    5.12    B :: "real"
    5.13 +However, such a solution would be cleanest w.r.t logics
    5.14  *}
    5.15  
    5.16  axiomatization where
    5.17    ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
    5.18    equival_trans_2nd_order: "( n/(a*b) = A/a + B/b ) = ( n = A*b + B*a )"
    5.19  
    5.20 -
    5.21  ML {*
    5.22  val ansatz_rls = prep_rls(
    5.23    Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    5.24 @@ -158,7 +156,6 @@
    5.25  *}
    5.26  
    5.27  
    5.28 -
    5.29  text {*rule set for partial fractions*}
    5.30  ML {*
    5.31  val partial_fraction = 

     6.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Jan 05 17:43:48 2012 +0100
     6.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Sat Jan 07 10:06:06 2012 +0100
     6.3 @@ -279,30 +279,6 @@
     6.4     replace all occurrences of lhs in the term with rhs;
     6.5     thus the order or equalities matters: put variables in lhs first. *)
     6.6  fun rewrite_terms_ thy ord erls equs t =
     6.7 -    let (*val _=tracing("### rewrite_terms_ equs= '"^terms2str equs^"' ..."^
     6.8 -		      term_detail2str (hd equs)^
     6.9 -		      "### rewrite_terms_ t= '"^term2str t^"' ..."^
    6.10 -		      term_detail2str t);*)
    6.11 -	fun rew_ (t', asm') [] _ = (t', asm')
    6.12 -	  (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], equs, t);
    6.13 -	     2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
    6.14 -	     rew_ (t', asm') (r::rs) t;
    6.15 -	     *)
    6.16 -	  | rew_ (t', asm') (rules as r::rs) t =
    6.17 -	    let val _ = tracing("rew_ "^term2str t);
    6.18 -		val (t'', asm'', lrd, rew) = 
    6.19 -		    rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
    6.20 -	    in if rew 
    6.21 -	       then (tracing ("true  rew_ " ^ term2str t'');
    6.22 -		   rew_ (t'', asm' @ asm'') rules t'')
    6.23 -	       else (tracing ("false rew_ " ^ term2str t'');
    6.24 -		   rew_ (t', asm') rs t')
    6.25 -	    end
    6.26 -	val (t'', asm'') = rew_ (e_term, []) equs t
    6.27 -    in if t'' = e_term 
    6.28 -       then NONE else SOME (t'', asm'')
    6.29 -    end;
    6.30 -fun rewrite_terms_ thy ord erls equs t =
    6.31    let
    6.32  	  fun rew_ (t', asm') [] _ = (t', asm')
    6.33  	    | rew_ (t', asm') (rules as r::rs) t =

     7.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Thu Jan 05 17:43:48 2012 +0100
     7.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Sat Jan 07 10:06:06 2012 +0100
     7.3 @@ -179,7 +179,7 @@
     7.4      (*val _= tracing("### upd_env: = "^(subst2str env'));*)
     7.5    in env' end;
     7.6  
     7.7 -(*.substitute the scripts environment in a leaf of the scripts parse-tree
     7.8 +(*.substitute the script's environment in a leaf of the script's parse-tree
     7.9     and attach the curried argument of a tactic, if any.
    7.10     a leaf is either a tactic or an 'exp' in 'let v = expr'
    7.11     where 'exp' does not contain a tactic.

     8.1 --- a/src/Tools/isac/ProgLang/termC.sml	Thu Jan 05 17:43:48 2012 +0100
     8.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Sat Jan 07 10:06:06 2012 +0100
     8.3 @@ -233,7 +233,7 @@
     8.4      handle _ => error ("free2int: "^term_detail2str t))
     8.5    | free2int t = error ("free2int: "^term_detail2str t);
     8.6  
     8.7 -(*compare Logic.unvarify_global: rejects Free*)
     8.8 +(*compare Logic.unvarify_global, which rejects Free*)
     8.9  fun var2free (t as Const(s,T)) = t
    8.10    | var2free (t as Free(s,T)) = t
    8.11    | var2free (Var((s,i),T)) = Free(s,T)

     9.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Jan 05 17:43:48 2012 +0100
     9.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jan 07 10:06:06 2012 +0100
     9.3 @@ -314,7 +314,6 @@
     9.4  
     9.5  val prod = mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; 
     9.6  term2str prod = "(x + 1) * (x + 2) * (x + 3)";
     9.7 -
     9.8  *)
     9.9  
    9.10  fun factors_from_solution sol = 
    9.11 @@ -493,8 +492,7 @@
    9.12    the right-hand-side must also occur on the left-hand-side of the rule:
    9.13    A, B, etc don't.
    9.14    Thus the rewriter marks these variables with question marks: ?A, ?B, etc.
    9.15 -  These question marks are dropped by a function, which can be included 
    9.16 -  into a ruleset by Calc.
    9.17 +  These question marks can be dropped by "fun drop_questionmarks".
    9.18    *}
    9.19  ML {*
    9.20  val ansatz_rls = prep_rls(
    9.21 @@ -507,7 +505,6 @@
    9.22  	 scr = EmptyScr});
    9.23  *}
    9.24  ML {*
    9.25 -trace_rewrite := true;
    9.26  val SOME (ttttt,_) = rewrite_set_ @{theory Isac} false ansatz_rls expr';
    9.27  *}
    9.28  ML {*
    9.29 @@ -613,8 +610,6 @@
    9.30  
    9.31  subsubsection {*substitute expression with solutions*}
    9.32  ML {*
    9.33 -f2str fa;
    9.34 -f2str fb
    9.35  *}
    9.36  ML {*thy*}
    9.37  
    9.38 @@ -980,12 +975,18 @@
    9.39  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    9.40  (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)
    9.41  *}
    9.42 +
    9.43 +ML {*
    9.44 +show_pt pt;
    9.45 +*}
    9.46 +
    9.47  ML {*
    9.48  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    9.49  (*([7], Res), 24 = ?A * 3 / 4*)
    9.50  show_pt pt;
    9.51  *}
    9.52  
    9.53 +
    9.54  ML {*
    9.55  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    9.56  val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    10.1 --- a/test/Tools/isac/Interpret/ctree.sml	Thu Jan 05 17:43:48 2012 +0100
    10.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Sat Jan 07 10:06:06 2012 +0100
    10.3 @@ -46,6 +46,7 @@
    10.4  "=====new ptree 6 minisubpbl intersteps ==========================";
    10.5  "-------------- get_allpos' new ----------------------------------";
    10.6  "-------------- cut_tree new (from ptree above)-------------------";
    10.7 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
    10.8  "-----------------------------------------------------------------";
    10.9  "-----------------------------------------------------------------";
   10.10  "-----------------------------------------------------------------";
   10.11 @@ -1373,3 +1374,42 @@
   10.12  show_pt pt;
   10.13  *)
   10.14  ========== inhibit exn AK110726 ==============================================*)
   10.15 +
   10.16 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
   10.17 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
   10.18 +"-------------- subst2subs subs2subst sube2subst subte2subst -----";
   10.19 +val subst = [(str2term "bdv", str2term "x"), (str2term "err", str2term "0")];
   10.20 +
   10.21 +if ["bdv = x", "err = 0"] = subte2sube [str2term "bdv = x", str2term "err = 0"] then ()
   10.22 +else error "subte2sube broken";
   10.23 +
   10.24 +subst2subs : (term * term) list -> string list;
   10.25 +if subst2subs subst = ["(bdv, x)", "(err, 0)"] then ()
   10.26 +else error "subst2subs broken";
   10.27 +
   10.28 +subst2subs' : (term * term) list -> (string * string) list;
   10.29 +if subst2subs' subst = [("bdv", "x"), ("err", "0")] then ()
   10.30 +else error "subst2subs' broken";
   10.31 +
   10.32 +subs2subst : theory -> string list -> (term * term) list;
   10.33 +val [(i1, v1), (i2, v2)] = subs2subst thy ["(bdv, x)", "(err, 0)"];
   10.34 +if term2str i1 = "bdv" andalso term2str v1 = "x" andalso 
   10.35 +  term2str i2 = "err" andalso term2str v2 = "0" then ()
   10.36 +else error "subs2subst broken";
   10.37 +
   10.38 +sube2subst : theory -> string list -> (term * term) list;
   10.39 +val [(i1, v1), (i2, v2)] = sube2subst thy ["bdv = x", "err = 0"];
   10.40 +if term2str i1 = "bdv" andalso term2str v1 = "x" andalso 
   10.41 +  term2str i2 = "err" andalso term2str v2 = "0" then ()
   10.42 +else error "sube2subst broken";
   10.43 +
   10.44 +sube2subte : string list -> term list;
   10.45 +val [eq1, eq2] = sube2subte ["bdv = x", "err = 0"];
   10.46 +if term2str eq1 = "bdv = x" andalso term2str eq2 = "err = 0" then ()
   10.47 +else error "sube2subte broken";
   10.48 +
   10.49 +val [(i1, v1), (i2, v2)] = subte2subst [str2term "bdv = x", str2term "err = 0"];
   10.50 +if term2str i1 = "bdv" andalso term2str v1 = "x" andalso 
   10.51 +  term2str i2 = "err" andalso term2str v2 = "0" then ()
   10.52 +else error "subte2subst broken";
   10.53 +

    11.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Jan 05 17:43:48 2012 +0100
    11.2 +++ b/test/Tools/isac/Test_Isac.thy	Sat Jan 07 10:06:06 2012 +0100
    11.3 @@ -181,6 +181,7 @@
    11.4    ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
    11.5    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    11.6    ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
    11.7 +  ML {*"%%%%%%%%%%%%%%%%% if nothing is read.  %%%%%%%%%%%%%%%%%";*}
    11.8    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    11.9  
   11.10  end