1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sun Jul 21 15:15:50 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Jul 22 13:52:18 2013 +0200
1.3 @@ -284,8 +284,7 @@
1.4 (*WN.11.03: + dont take first inter<>[]*)
1.5 fun seek_oridts ctxt sel (d,ts) [] =
1.6 ("seek_oridts: input ('" ^
1.7 - (Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))) ^
1.8 - "') not found in oris (typed)",
1.9 + (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",
1.10 (0, [], sel, d, ts),
1.11 [])
1.12 | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
1.13 @@ -295,20 +294,13 @@
1.14
1.15 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.16 fun seek_orits ctxt sel ts [] =
1.17 - ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
1.18 - ctxt)) ts) ^
1.19 - "') not found in oris (typed)", e_ori_, [])
1.20 + ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
1.21 + "') not found in oris (typed)", e_ori_, [])
1.22 | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.23 if sel = sel' andalso (inter op = ts ts') <> []
1.24 then if sel = sel'
1.25 - then ("",
1.26 - (id,vat,sel,d, inter op = ts ts'):ori,
1.27 - ts')
1.28 - else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.29 - ctxt))) ts)
1.30 - ^ " not for " ^ sel,
1.31 - e_ori_,
1.32 - [])
1.33 + then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts')
1.34 + else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
1.35 else seek_orits ctxt sel ts oris;
1.36 (* false
1.37 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.38 @@ -478,20 +470,15 @@
1.39 (* val (_,_,fd,d,ts) = hd miss;
1.40 *)
1.41 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.42 - (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
1.43 - comp_dts) (d,[hd ts]) : cterm');
1.44 + (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');
1.45 (* val t = comp_dts (d,[hd ts]);
1.46 *)
1.47
1.48 (* get a term from ori, notyet input in itm.
1.49 the term from ori is thrown back to a string in order to reuse
1.50 machinery for immediate input by the user. *)
1.51 -fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.52 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.53 - (d, subtract op = (ts_in itm_) ts) : cterm');
1.54 -fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.55 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.56 - (d, subtract op = (ts_in itm_) ts) : cterm');
1.57 +fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.58 + (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
1.59
1.60 (* in FE dsc, not dat: this is in itms ...*)
1.61 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
1.62 @@ -514,9 +501,7 @@
1.63 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
1.64 *)
1.65 (f,(d,_))::itms =>
1.66 - SOME (f : string,
1.67 - ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.68 - comp_dts) (d, []) : cterm')
1.69 + SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
1.70 | _ => NONE end
1.71
1.72 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.73 @@ -684,43 +669,28 @@
1.74 *)
1.75 fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.76 case find_first (eq1 d) pbt of
1.77 - SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
1.78 - val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
1.79 - *)
1.80 + SOME (_,(_,pid)) =>
1.81 (case find_first (eq3 f d) itms of
1.82 - SOME (_,_,_,_,itm_) =>
1.83 - let
1.84 - val ts' = inter op = (ts_in itm_) ts;
1.85 - in if subset op = (ts, ts')
1.86 - then (((strs2str' o
1.87 - map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
1.88 - " already input", e_itm) (*2*)
1.89 - else ("",
1.90 - ori_2itm itm_ pid all (i,v,f,d,
1.91 - subtract op = ts' ts)) (*3,4*)
1.92 - end
1.93 - | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
1.94 - pid all (i,v,f,d,ts)) (*1*)
1.95 - )
1.96 - | NONE => ("", ori_2itm (Sup (d,ts))
1.97 - e_term all (i,v,f,d,ts));
1.98 + SOME (_,_,_,_,itm_) =>
1.99 + let
1.100 + val ts' = inter op = (ts_in itm_) ts;
1.101 + in
1.102 + if subset op = (ts, ts')
1.103 + then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)
1.104 + else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
1.105 + end
1.106 + | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts))) (*1*)
1.107 + | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));
1.108
1.109 fun test_types ctxt (d,ts) =
1.110 let
1.111 - (*val s = !show_types; val _ = show_types:= true;*)
1.112 val opt = (try comp_dts) (d,ts);
1.113 val msg = case opt of
1.114 SOME _ => ""
1.115 - | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.116 - " " ^
1.117 - ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.118 - ctxt))) ts)
1.119 - ^ " is illtyped");
1.120 - (*val _ = show_types:= s*)
1.121 + | NONE => (term_to_string' ctxt d ^ " " ^
1.122 + (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");
1.123 in msg end;
1.124
1.125 -
1.126 -
1.127 fun maxl [] = error "maxl of []"
1.128 | maxl (y::ys) =
1.129 let fun mx x [] = x
1.130 @@ -747,9 +717,8 @@
1.131 if d = e_term
1.132 then
1.133 if not (subset op = (map typeless ts, map typeless ots))
1.134 - then (("terms '" ^ ((strs2str' o
1.135 - (map (Print_Mode.setmp [] (Syntax.string_of_term ctxt)))) ts) ^
1.136 - "' not in example (typeless)"), e_ori_, [])
1.137 + then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
1.138 + "' not in example (typeless)", e_ori_, [])
1.139 else
1.140 (case seek_orits ctxt sel ts ori of
1.141 ("", ori_ as (_,_,_,d,ts), all) =>
1.142 @@ -760,11 +729,9 @@
1.143 else
1.144 if member op = (map #4 ori) d
1.145 then seek_oridts ctxt sel (d,ts) ori
1.146 - else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.147 - " not in example", (0, [], sel, d, ts), [])
1.148 + else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
1.149 end;
1.150
1.151 -
1.152 (*. for return-value of appl_add .*)
1.153 datatype additm =
1.154 Add of itm
1.155 @@ -1568,16 +1535,12 @@
1.156 (*fun tag_form thy (formal, given) = cterm_of thy
1.157 (((head_of o term_of) given) $ (term_of formal)); WN100819*)
1.158 fun tag_form thy (formal, given) =
1.159 - (let val gf = (head_of given) $ formal;
1.160 - val _ = cterm_of thy gf
1.161 - in gf end)
1.162 - handle _ =>
1.163 - error ("calchead.tag_form: " ^
1.164 - Print_Mode.setmp [] (Syntax.string_of_term
1.165 - (thy2ctxt thy)) given ^ " .. " ^
1.166 - Print_Mode.setmp [] (Syntax.string_of_term
1.167 - (thy2ctxt thy)) formal ^
1.168 - " ..types do not match");
1.169 + (let
1.170 + val gf = (head_of given) $ formal;
1.171 + val _ = cterm_of thy gf
1.172 + in gf end)
1.173 + handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1.174 + " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
1.175 (* val formal = (the o (parse thy)) "[R::real]";
1.176 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
1.177 > tag_form thy (formal, given);
1.178 @@ -1585,10 +1548,8 @@
1.179 *)
1.180
1.181 fun chktyp thy (n, fs, gs) =
1.182 - ((writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.183 - (nth n)) fs;
1.184 - (writeln o (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.185 - (nth n)) gs;
1.186 + ((writeln o (term_to_string''' thy) o (nth n)) fs;
1.187 + (writeln o (term_to_string''' thy) o (nth n)) gs;
1.188 tag_form thy (nth n fs, nth n gs));
1.189 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1.190
2.1 --- a/src/Tools/isac/Interpret/inform.sml Sun Jul 21 15:15:50 2013 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Jul 22 13:52:18 2013 +0200
2.3 @@ -200,36 +200,40 @@
2.4
2.5 (*re-parse itms with a new thy and prepare for checking with ori list*)
2.6 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
2.7 -(* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
2.8 - *)
2.9 - (let val t = comp_dts (d,ts);
2.10 - val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.11 - (*this ^ should raise the exn on unability of re-parsing dts*)
2.12 - in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.13 + (let
2.14 + val t = comp_dts (d,ts);
2.15 + val s = term_to_string''' dI t;
2.16 + (*this ^ should raise the exn on unability of re-parsing dts*)
2.17 + in itm end
2.18 + handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.19 | parsitm dI (itm as (i,v,b,f, Syn str)) =
2.20 (let val t = (term_of o the o (parse dI)) str
2.21 - in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
2.22 + in (i,v,b,f, Par str) end
2.23 + handle _ => (i,v,b,f, Syn str))
2.24 | parsitm dI (itm as (i,v,b,f, Typ str)) =
2.25 (let val t = (term_of o the o (parse dI)) str
2.26 - in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
2.27 + in (i,v,b,f, Par str) end
2.28 + handle _ => (i,v,b,f, Syn str))
2.29 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
2.30 (let val t = comp_dts (d,ts);
2.31 - val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.32 + val s = term_to_string''' dI t;
2.33 (*this ^ should raise the exn on unability of re-parsing dts*)
2.34 - in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.35 + in itm end
2.36 + handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.37 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
2.38 (let val t = comp_dts (d,ts);
2.39 - val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.40 + val s = term_to_string''' dI t;
2.41 (*this ^ should raise the exn on unability of re-parsing dts*)
2.42 - in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.43 + in itm end
2.44 + handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.45 | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
2.46 (let val t = d $ t';
2.47 - val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.48 + val s = term_to_string''' dI t;
2.49 (*this ^ should raise the exn on unability of re-parsing dts*)
2.50 - in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.51 + in itm end
2.52 + handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.53 | parsitm dI (itm as (i,v,_,f, Par _)) =
2.54 - error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
2.55 - "): Par should be internal");
2.56 + error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
2.57
2.58 (*separate a list to a pair of elements that do NOT satisfy the predicate,
2.59 and of elements that satisfy the predicate, i.e. (false, true)*)
3.1 --- a/src/Tools/isac/Interpret/mstools.sml Sun Jul 21 15:15:50 2013 +0200
3.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Jul 22 13:52:18 2013 +0200
3.3 @@ -379,13 +379,12 @@
3.4 WN.9.5.03: penv-concept stalled, immediately generate script env !
3.5 but [#0, epsilon] only outcommented for eventual reconsideration
3.6 *)
3.7 -type penv = (term (*err_*)
3.8 - * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
3.9 +type penv = (term (*err_*)
3.10 + * (term list) (*[#0, epsilon] 9.5.03 outcommented*)
3.11 ) list;
3.12 fun pen2str ctxt (t, ts) =
3.13 - pair2str (Print_Mode.setmp [] (Syntax.string_of_term ctxt) t,
3.14 - (strs2str' o
3.15 - map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts);
3.16 + pair2str (term_to_string' ctxt t,
3.17 + (strs2str' o map (term_to_string' ctxt)) ts);
3.18 fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;
3.19
3.20 (*
3.21 @@ -600,9 +599,7 @@
3.22 then [v] (*eg. [r=Arbfix]*)
3.23 else (case v of (*eg. eps=#0*)
3.24 (Const ("HOL.eq",_) $ l $ r) => [r,l]
3.25 - | _ =>
3.26 - error ("pbl_ids Tools.nam: no equality "
3.27 - ^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) v))
3.28 + | _ => error ("pbl_ids Tools.nam: no equality " ^ term_to_string' ctxt v))
3.29 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]
3.30 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]
3.31 | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]
3.32 @@ -800,21 +797,15 @@
3.33 | item2str (Missing s) ="Missing " ^ s;
3.34 (*make string for error-msgs*)
3.35 fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
3.36 - "Cor " ^
3.37 - Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)) ^
3.38 - " ," ^ pen2str ctxt penv
3.39 - | itm_2str_ ctxt (Syn c) = "Syn " ^ c
3.40 - | itm_2str_ ctxt (Typ c) = "Typ " ^ c
3.41 + "Cor " ^ term_to_string' ctxt (comp_dts (d,ts)) ^ " ," ^ pen2str ctxt penv
3.42 + | itm_2str_ ctxt (Syn c) = "Syn " ^ c
3.43 + | itm_2str_ ctxt (Typ c) = "Typ " ^ c
3.44 | itm_2str_ ctxt (Inc ((d,ts), penv)) =
3.45 - "Inc " ^
3.46 - Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)) ^
3.47 - " ," ^ pen2str ctxt penv
3.48 + "Inc " ^ term_to_string' ctxt (comp_dts (d,ts)) ^ " ," ^ pen2str ctxt penv
3.49 | itm_2str_ ctxt (Sup (d,ts)) =
3.50 - "Sup " ^
3.51 - Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))
3.52 - | itm_2str_ ctxt (Mis (d,pid))=
3.53 - "Mis "^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) d ^
3.54 - " " ^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) pid
3.55 + "Sup " ^ term_to_string' ctxt (comp_dts (d,ts))
3.56 + | itm_2str_ ctxt (Mis (d,pid)) =
3.57 + "Mis "^ term_to_string' ctxt d ^ " " ^ term_to_string' ctxt pid
3.58 | itm_2str_ ctxt (Par s) = "Trm "^s;
3.59 fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;
3.60 fun itm2str_ ctxt ((i,is,b,s,itm_):itm) =
4.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Jul 21 15:15:50 2013 +0200
4.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Jul 22 13:52:18 2013 +0200
4.3 @@ -79,7 +79,7 @@
4.4 (*ML {*
4.5 val trm = @{term "k ~= 0 ==> k * m / (k * n) = m / n"};
4.6 (tracing o
4.7 - (Print_Mode.setmp [] (Syntax.string_of_term @{context}))) (sym_trm trm);
4.8 + (term_to_string')) (sym_trm trm);
4.9 "~ k = (0::'a) ==> m / n = k * m / (k * n)"
4.10 *}*)
4.11
5.1 --- a/src/Tools/isac/Interpret/script.sml Sun Jul 21 15:15:50 2013 +0200
5.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Jul 22 13:52:18 2013 +0200
5.3 @@ -215,17 +215,9 @@
5.4 fun init_form thy (Prog sc) env =
5.5 (case get_stac thy sc of
5.6 NONE => NONE
5.7 - (*error ("init_form: no 1st stac in "^
5.8 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) sc))*)
5.9 | SOME stac => SOME (subst_atomic env stac))
5.10 | init_form _ _ _ = error "init_form: no match";
5.11
5.12 -(* use"ME/script.sml";
5.13 - use"script.sml";
5.14 - *)
5.15 -
5.16 -
5.17 -
5.18 (*the 'iteration-argument' of a stac (args not eval)*)
5.19 fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v
5.20 | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v
5.21 @@ -236,9 +228,7 @@
5.22 | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term
5.23 | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
5.24 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
5.25 - | itr_arg thy t = error
5.26 - ("itr_arg not impl. for " ^
5.27 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt (assoc_thy thy))) t));
5.28 + | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);
5.29 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
5.30 > itr_arg "Script" t;
5.31 val it = Free ("e_","RealDef.real") : term
5.32 @@ -291,19 +281,15 @@
5.33 (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
5.34 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
5.35 fun mk_arg thy d [] =
5.36 - error ("mk_arg: no data for " ^
5.37 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d))
5.38 + error ("mk_arg: no data for " ^ term_to_string''' thy d)
5.39 | mk_arg thy d [t] =
5.40 (case dsc_valT d of
5.41 - "una" => [t]
5.42 - | "nam" =>
5.43 - [case t of
5.44 - r as (Const ("HOL.eq",_) $ _ $ _) => r
5.45 - | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality "^
5.46 - (Print_Mode.setmp [] (Syntax.string_of_term
5.47 - (thy2ctxt thy)) t))]
5.48 - | s => error ("mk_arg: not impl. for "^s))
5.49 -
5.50 + "una" => [t]
5.51 + | "nam" =>
5.52 + [case t of
5.53 + r as (Const ("HOL.eq",_) $ _ $ _) => r
5.54 + | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality " ^ term_to_string''' thy t)]
5.55 + | s => error ("mk_arg: not impl. for "^s))
5.56 | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
5.57 (*
5.58 val d = d_in itm_;
5.59 @@ -341,7 +327,7 @@
5.60 > val mI = ("Script","sqrt-equ-test");
5.61 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
5.62 > val ts = itms2args thy mI itms;
5.63 -> map (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) ts;
5.64 +> map (term_to_string''' thy) ts;
5.65 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
5.66 *)
5.67
5.68 @@ -388,9 +374,8 @@
5.69 (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
5.70
5.71 | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $
5.72 - (set as Const ("Set.Collect",_) $ Abs (_,_,pred))) =
5.73 - (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term
5.74 - (thy2ctxt thy)) pred), (*set*)Empty_Tac_)
5.75 + (set as Const ("Set.Collect",_) $ Abs (_,_,pred))) =
5.76 + (Check_elementwise (term_to_string''' thy pred), (*set*)Empty_Tac_)
5.77
5.78 | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) =
5.79 (Or_to_List, Empty_Tac_)
5.80 @@ -436,10 +421,8 @@
5.81 val f = subpbl (strip_thy dI) pI
5.82 in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
5.83 end
5.84 -
5.85 | stac2tac_ pt thy t = error
5.86 - ("stac2tac_ TODO: no match for " ^
5.87 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t));
5.88 + ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
5.89
5.90 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
5.91
5.92 @@ -696,8 +679,7 @@
5.93
5.94 fun make_rule thy t =
5.95 let val ct = cterm_of thy (Trueprop $ t)
5.96 - in Thm (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
5.97 - (term_of ct), make_thm ct) end;
5.98 + in Thm (term_to_string''' thy (term_of ct), make_thm ct) end;
5.99
5.100 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
5.101 *)
6.1 --- a/src/Tools/isac/Knowledge/Atools.thy Sun Jul 21 15:15:50 2013 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Mon Jul 22 13:52:18 2013 +0200
6.3 @@ -344,16 +344,12 @@
6.4 (Const (op0,t0) $ t1 $ t2 )) thy =
6.5 if t1 = t2
6.6 then SOME (mk_thmid thmid op0
6.7 - ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
6.8 - (thy2ctxt thy)) t1) ^ ")")
6.9 - ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
6.10 - (thy2ctxt thy)) t2) ^ ")"),
6.11 + ("(" ^ (term_to_string''' thy t1) ^ ")")
6.12 + ("(" ^ (term_to_string''' thy t2) ^ ")"),
6.13 Trueprop $ (mk_equality (t, @{term True})))
6.14 else SOME (mk_thmid thmid op0
6.15 - ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
6.16 - (thy2ctxt thy)) t1) ^ ")")
6.17 - ("(" ^ (Print_Mode.setmp [] (Syntax.string_of_term
6.18 - (thy2ctxt thy)) t2) ^ ")"),
6.19 + ("(" ^ (term_to_string''' thy t1) ^ ")")
6.20 + ("(" ^ (term_to_string''' thy t2) ^ ")"),
6.21 Trueprop $ (mk_equality (t, @{term False})))
6.22 | eval_ident _ _ _ _ = NONE;
6.23 (* TODO
6.24 @@ -377,28 +373,19 @@
6.25 (*.evaluate identity of terms, which stay ready for evaluation in turn;
6.26 thus returns False only for atoms.*)
6.27 (*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
6.28 -fun eval_equal (thmid : string) "HOL.eq" (t as
6.29 - (Const (op0,t0) $ t1 $ t2 )) thy =
6.30 - if t1 = t2
6.31 - then SOME (mk_thmid thmid op0
6.32 - ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
6.33 - (thy2ctxt thy)) t1 ^
6.34 - ")")
6.35 - ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
6.36 - (thy2ctxt thy)) t2 ^
6.37 - ")"),
6.38 - Trueprop $ (mk_equality (t, @{term True})))
6.39 - else (case (is_atom t1, is_atom t2) of
6.40 - (true, true) =>
6.41 - SOME (mk_thmid thmid op0
6.42 - ("(" ^ Print_Mode.setmp [] (Syntax.string_of_term
6.43 - (thy2ctxt thy)) t1^
6.44 - ")") ("(" ^
6.45 - Print_Mode.setmp [] (Syntax.string_of_term
6.46 - (thy2ctxt thy)) t2^
6.47 - ")"),
6.48 - Trueprop $ (mk_equality (t, @{term False})))
6.49 - | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
6.50 +fun eval_equal (thmid : string) "HOL.eq" (t as (Const (op0,t0) $ t1 $ t2 )) thy =
6.51 + if t1 = t2
6.52 + then SOME (mk_thmid thmid op0
6.53 + ("(" ^ term_to_string''' thy t1 ^ ")")
6.54 + ("(" ^ term_to_string''' thy t2 ^ ")"),
6.55 + Trueprop $ (mk_equality (t, @{term True})))
6.56 + else (case (is_atom t1, is_atom t2) of
6.57 + (true, true) =>
6.58 + SOME (mk_thmid thmid op0
6.59 + ("(" ^ term_to_string''' thy t1 ^ ")")
6.60 + ("(" ^ term_to_string''' thy t2 ^ ")"),
6.61 + Trueprop $ (mk_equality (t, @{term False})))
6.62 + | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
6.63 | eval_equal _ _ _ _ = NONE; (* error-exit *)
6.64 (*
6.65 val t = str2term "x ~= 0";
7.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Jul 21 15:15:50 2013 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Jul 22 13:52:18 2013 +0200
7.3 @@ -301,10 +301,8 @@
7.4 ML {*(*1*) Free ("123.456", HOLogic.realT) *}
7.5 ML {*(*2*)
7.6 val unknown = filter ((curry op= "??.unknown") o fst) isacrlsthms;
7.7 -unknown |> nth 1 |> snd
7.8 - |> Print_Mode.setmp [] (Syntax.string_of_term (Proof_Context.init_global @{theory}));
7.9 -unknown |> nth 2 |> snd
7.10 - |> Print_Mode.setmp [] (Syntax.string_of_term (Proof_Context.init_global @{theory}));
7.11 +unknown |> nth 1 |> snd |> term_to_string''' @{theory};
7.12 +unknown |> nth 2 |> snd |> term_to_string''' @{theory};
7.13 (*but these seem ok:*)
7.14 Thm.get_name_hint @{thm add_0};
7.15 Thm.get_name_hint (num_str @{thm add_0});
8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Jul 21 15:15:50 2013 +0200
8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Jul 22 13:52:18 2013 +0200
8.3 @@ -128,42 +128,34 @@
8.4 | size_of_term' _ = 1;
8.5
8.6 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
8.7 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
8.8 + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
8.9 | term_ord' pr thy (t, u) =
8.10 - (if pr then
8.11 - let
8.12 - val (f, ts) = strip_comb t and (g, us) = strip_comb u;
8.13 - val _ = tracing ("t= f@ts= \"" ^
8.14 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) f) ^
8.15 - "\" @ \"[" ^
8.16 - (commas (map (Print_Mode.setmp [] (Syntax.string_of_term
8.17 - (thy2ctxt thy))) ts)) ^ "]\"");
8.18 - val _ = tracing ("u= g@us= \"" ^
8.19 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) g) ^
8.20 - "\" @ \"[" ^
8.21 - (commas (map (Print_Mode.setmp [] (Syntax.string_of_term
8.22 - (thy2ctxt thy))) us)) ^ "]\"");
8.23 - val _ = tracing ("size_of_term(t,u)= (" ^
8.24 - (string_of_int (size_of_term' t)) ^ ", " ^
8.25 - (string_of_int (size_of_term' u)) ^ ")");
8.26 - val _ = tracing ("hd_ord(f,g) = " ^ ((pr_ord o hd_ord) (f,g)));
8.27 - val _ = tracing ("terms_ord (ts,us) = " ^
8.28 - ((pr_ord o terms_ord str false) (ts,us)));
8.29 - val _=tracing("-------");
8.30 - in () end
8.31 - else ();
8.32 - case int_ord (size_of_term' t, size_of_term' u) of
8.33 - EQUAL =>
8.34 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
8.35 - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
8.36 - | ord => ord)
8.37 - end
8.38 + (if pr
8.39 + then
8.40 + let
8.41 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
8.42 + val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
8.43 + commas (map (term_to_string''' thy) ts) ^ "]\"");
8.44 + val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
8.45 + commas (map (term_to_string''' thy) us) ^ "]\"");
8.46 + val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
8.47 + string_of_int (size_of_term' u) ^ ")");
8.48 + val _ = tracing ("hd_ord(f,g) = " ^ ((pr_ord o hd_ord) (f,g)));
8.49 + val _ = tracing ("terms_ord (ts,us) = " ^(pr_ord o terms_ord str false) (ts,us));
8.50 + val _=tracing("-------");
8.51 + in () end
8.52 + else ();
8.53 + case int_ord (size_of_term' t, size_of_term' u) of
8.54 + EQUAL =>
8.55 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
8.56 + in (case hd_ord (f, g) of
8.57 + EQUAL => (terms_ord str pr) (ts, us)
8.58 + | ord => ord)
8.59 + end
8.60 | ord => ord)
8.61 and hd_ord (f, g) = (* ~ term.ML *)
8.62 - prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f,
8.63 - dest_hd' g)
8.64 -and terms_ord str pr (ts, us) =
8.65 - list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
8.66 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
8.67 +and terms_ord str pr (ts, us) = list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
8.68 (**)
8.69 in
8.70 (**)
9.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Jul 21 15:15:50 2013 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Jul 22 13:52:18 2013 +0200
9.3 @@ -62,9 +62,8 @@
9.4 fun eval_factors_from_solution (thmid:string) _
9.5 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
9.6 ((let val prod = factors_from_solution sol
9.7 - in SOME (mk_thmid thmid ""
9.8 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
9.9 - Trueprop $ (mk_equality (t, prod)))
9.10 + in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",
9.11 + Trueprop $ (mk_equality (t, prod)))
9.12 end)
9.13 handle _ => NONE)
9.14 | eval_factors_from_solution _ _ _ _ = NONE;
9.15 @@ -79,9 +78,8 @@
9.16 then
9.17 let
9.18 val tm' = var2free tm
9.19 - in SOME (mk_thmid thmid ""
9.20 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) tm') "",
9.21 - Trueprop $ (mk_equality (t, tm')))
9.22 + in SOME (mk_thmid thmid "" (term_to_string''' thy tm') "",
9.23 + Trueprop $ (mk_equality (t, tm')))
9.24 end
9.25 else NONE
9.26 | eval_drop_questionmarks _ _ _ _ = NONE;
10.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Jul 21 15:15:50 2013 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Jul 22 13:52:18 2013 +0200
10.3 @@ -444,31 +444,21 @@
10.4 | size_of_term' _ = 1;
10.5
10.6 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
10.7 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
10.8 + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
10.9 | term_ord' pr thy (t, u) =
10.10 - (if pr then
10.11 - let
10.12 - val (f, ts) = strip_comb t and (g, us) = strip_comb u;
10.13 - val _ = tracing ("t= f@ts= \"" ^
10.14 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) f) ^
10.15 - "\" @ \"[" ^
10.16 - (commas (map (Print_Mode.setmp [] (Syntax.string_of_term
10.17 - (thy2ctxt thy))) ts)) ^
10.18 - "]\"");
10.19 - val _ = tracing("u= g@us= \""^
10.20 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) g) ^
10.21 - "\" @ \"[" ^
10.22 - (commas (map (Print_Mode.setmp [] (Syntax.string_of_term
10.23 - (thy2ctxt thy))) us)) ^
10.24 - "]\"");
10.25 - val _ = tracing ("size_of_term(t,u)= (" ^
10.26 - (string_of_int (size_of_term' t)) ^ ", " ^
10.27 - (string_of_int (size_of_term' u)) ^ ")");
10.28 - val _ = tracing ("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
10.29 - val _ = tracing ("terms_ord(ts,us) = " ^
10.30 - ((pr_ord o terms_ord str false) (ts, us)));
10.31 - val _ = tracing ("-------");
10.32 - in () end
10.33 + (if pr then
10.34 + let
10.35 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
10.36 + val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
10.37 + commas (map (term_to_string''' thy) ts) ^ "]\"");
10.38 + val _ = tracing("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
10.39 + commas (map (term_to_string''' thy) us) ^ "]\"");
10.40 + val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
10.41 + string_of_int (size_of_term' u) ^ ")");
10.42 + val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
10.43 + val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
10.44 + val _ = tracing ("-------");
10.45 + in () end
10.46 else ();
10.47 case int_ord (size_of_term' t, size_of_term' u) of
10.48 EQUAL =>
10.49 @@ -481,6 +471,7 @@
10.50 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
10.51 and terms_ord str pr (ts, us) =
10.52 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
10.53 +
10.54 in
10.55
10.56 fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
10.57 @@ -573,14 +564,10 @@
10.58 fun eval_is_polyexp (thmid:string) _
10.59 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
10.60 if is_polyexp arg
10.61 - then SOME (mk_thmid thmid ""
10.62 - (Print_Mode.setmp [] (Syntax.string_of_term
10.63 - (thy2ctxt thy)) arg) "",
10.64 - Trueprop $ (mk_equality (t, @{term True})))
10.65 - else SOME (mk_thmid thmid ""
10.66 - (Print_Mode.setmp [] (Syntax.string_of_term
10.67 - (thy2ctxt thy)) arg) "",
10.68 - Trueprop $ (mk_equality (t, @{term False})))
10.69 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
10.70 + Trueprop $ (mk_equality (t, @{term True})))
10.71 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
10.72 + Trueprop $ (mk_equality (t, @{term False})))
10.73 | eval_is_polyexp _ _ _ _ = NONE;
10.74
10.75 val expand_poly_rat_ =
10.76 @@ -1327,17 +1314,12 @@
10.77 fun eval_is_multUnordered (thmid:string) _
10.78 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
10.79 if is_multUnordered arg
10.80 - then SOME (mk_thmid thmid ""
10.81 - (Print_Mode.setmp [] (Syntax.string_of_term
10.82 - (thy2ctxt thy)) arg) "",
10.83 - Trueprop $ (mk_equality (t, @{term True})))
10.84 - else SOME (mk_thmid thmid ""
10.85 - (Print_Mode.setmp [] (Syntax.string_of_term
10.86 - (thy2ctxt thy)) arg) "",
10.87 - Trueprop $ (mk_equality (t, @{term False})))
10.88 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
10.89 + Trueprop $ (mk_equality (t, @{term True})))
10.90 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
10.91 + Trueprop $ (mk_equality (t, @{term False})))
10.92 | eval_is_multUnordered _ _ _ _ = NONE;
10.93
10.94 -
10.95 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
10.96 []:(rule * (term * term list)) list;
10.97 fun init_state (_:term) = e_rrlsstate;
10.98 @@ -1385,14 +1367,10 @@
10.99 fun eval_is_addUnordered (thmid:string) _
10.100 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
10.101 if is_addUnordered arg
10.102 - then SOME (mk_thmid thmid ""
10.103 - (Print_Mode.setmp [] (Syntax.string_of_term
10.104 - (thy2ctxt thy)) arg) "",
10.105 - Trueprop $ (mk_equality (t, @{term True})))
10.106 - else SOME (mk_thmid thmid ""
10.107 - (Print_Mode.setmp [] (Syntax.string_of_term
10.108 - (thy2ctxt thy)) arg) "",
10.109 - Trueprop $ (mk_equality (t, @{term False})))
10.110 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
10.111 + Trueprop $ (mk_equality (t, @{term True})))
10.112 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
10.113 + Trueprop $ (mk_equality (t, @{term False})))
10.114 | eval_is_addUnordered _ _ _ _ = NONE;
10.115
10.116 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
11.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun Jul 21 15:15:50 2013 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 22 13:52:18 2013 +0200
11.3 @@ -1329,45 +1329,39 @@
11.4 | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
11.5 | size_of_term' x _ = 1;
11.6
11.7 -
11.8 fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
11.9 - (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
11.10 + (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
11.11 | term_ord' x pr thy (t, u) =
11.12 - (if pr then
11.13 - let
11.14 - val (f, ts) = strip_comb t and (g, us) = strip_comb u;
11.15 - val _ = tracing ("t= f@ts= \"" ^
11.16 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) f) ^
11.17 - "\" @ \"[" ^
11.18 - (commas (map (Print_Mode.setmp [] (Syntax.string_of_term
11.19 - (thy2ctxt thy))) ts)) ^ "]\"");
11.20 - val _ = tracing ("u= g@us= \"" ^
11.21 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) g) ^
11.22 - "\" @ \"[" ^
11.23 - (commas(map (Print_Mode.setmp [] (Syntax.string_of_term
11.24 - (thy2ctxt thy))) us)) ^ "]\"");
11.25 - val _ = tracing ("size_of_term(t,u)= (" ^
11.26 - (string_of_int (size_of_term' x t)) ^ ", " ^
11.27 - (string_of_int (size_of_term' x u)) ^ ")");
11.28 - val _ = tracing ("hd_ord(f,g) = " ^
11.29 - ((pr_ord o (hd_ord x)) (f,g)));
11.30 - val _ = tracing ("terms_ord(ts,us) = " ^
11.31 - ((pr_ord o (terms_ord x) str false) (ts, us)));
11.32 - val _ = tracing ("-------");
11.33 - in () end
11.34 - else ();
11.35 - case int_ord (size_of_term' x t, size_of_term' x u) of
11.36 - EQUAL =>
11.37 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
11.38 - (case hd_ord x (f, g) of EQUAL => (terms_ord x str pr) (ts, us)
11.39 - | ord => ord)
11.40 - end
11.41 + (if pr
11.42 + then
11.43 + let
11.44 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
11.45 + val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
11.46 + commas (map (term_to_string''' thy) ts) ^ "]\"");
11.47 + val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
11.48 + commas(map (term_to_string''' thy) us) ^ "]\"");
11.49 + val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^
11.50 + string_of_int (size_of_term' x u) ^ ")");
11.51 + val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o (hd_ord x)) (f,g));
11.52 + val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o (terms_ord x) str false) (ts, us));
11.53 + val _ = tracing ("-------");
11.54 + in () end
11.55 + else ();
11.56 + case int_ord (size_of_term' x t, size_of_term' x u) of
11.57 + EQUAL =>
11.58 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
11.59 + in
11.60 + (case hd_ord x (f, g) of
11.61 + EQUAL => (terms_ord x str pr) (ts, us)
11.62 + | ord => ord)
11.63 + end
11.64 | ord => ord)
11.65 and hd_ord x (f, g) = (* ~ term.ML *)
11.66 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
11.67 int_ord (dest_hd' x f, dest_hd' x g)
11.68 and terms_ord x str pr (ts, us) =
11.69 list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);
11.70 +
11.71 in
11.72
11.73 fun ord_make_polynomial_in (pr:bool) thy subst tu =
12.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Jul 21 15:15:50 2013 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jul 22 13:52:18 2013 +0200
12.3 @@ -2061,13 +2061,21 @@
12.4 let
12.5 val vars=get_vars(t11) union get_vars(t12) union get_vars(t21) union get_vars(t22);
12.6 val t11'= Unsynchronized.ref (the(term2poly t11 vars));
12.7 +(* stopped Test_Isac.thy ...
12.8 val _= tracing"### add_fract: done t11"
12.9 +*)
12.10 val t12'= Unsynchronized.ref (the(term2poly t12 vars));
12.11 +(* stopped Test_Isac.thy ...
12.12 val _= tracing"### add_fract: done t12"
12.13 +*)
12.14 val t21'= Unsynchronized.ref (the(term2poly t21 vars));
12.15 +(* stopped Test_Isac.thy ...
12.16 val _= tracing"### add_fract: done t21"
12.17 +*)
12.18 val t22'= Unsynchronized.ref (the(term2poly t22 vars));
12.19 +(* stopped Test_Isac.thy ...
12.20 val _= tracing"### add_fract: done t22"
12.21 +*)
12.22 val den= Unsynchronized.ref [];
12.23 val nom= Unsynchronized.ref [];
12.24 val m1= Unsynchronized.ref [];
12.25 @@ -2838,14 +2846,10 @@
12.26 fun eval_is_expanded (thmid:string) _
12.27 (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
12.28 if is_expanded arg
12.29 - then SOME (mk_thmid thmid ""
12.30 - (Print_Mode.setmp [] (Syntax.string_of_term
12.31 - (thy2ctxt thy)) arg) "",
12.32 - Trueprop $ (mk_equality (t, @{term True})))
12.33 - else SOME (mk_thmid thmid ""
12.34 - (Print_Mode.setmp [] (Syntax.string_of_term
12.35 - (thy2ctxt thy)) arg) "",
12.36 - Trueprop $ (mk_equality (t, @{term False})))
12.37 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
12.38 + Trueprop $ (mk_equality (t, @{term True})))
12.39 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
12.40 + Trueprop $ (mk_equality (t, @{term False})))
12.41 | eval_is_expanded _ _ _ _ = NONE;
12.42
12.43 val rational_erls =
12.44 @@ -3446,14 +3450,10 @@
12.45 fun eval_is_ratpolyexp (thmid:string) _
12.46 (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
12.47 if is_ratpolyexp arg
12.48 - then SOME (mk_thmid thmid ""
12.49 - (Print_Mode.setmp [] (Syntax.string_of_term
12.50 - (thy2ctxt thy)) arg) "",
12.51 - Trueprop $ (mk_equality (t, @{term True})))
12.52 - else SOME (mk_thmid thmid ""
12.53 - (Print_Mode.setmp [] (Syntax.string_of_term
12.54 - (thy2ctxt thy)) arg) "",
12.55 - Trueprop $ (mk_equality (t, @{term False})))
12.56 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
12.57 + Trueprop $ (mk_equality (t, @{term True})))
12.58 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
12.59 + Trueprop $ (mk_equality (t, @{term False})))
12.60 | eval_is_ratpolyexp _ _ _ _ = NONE;
12.61
12.62 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
12.63 @@ -3461,23 +3461,19 @@
12.64 (t as Const ("Rational.get_denominator", _) $
12.65 (Const ("Fields.inverse_class.divide", _) $ num $
12.66 denom)) thy =
12.67 - SOME (mk_thmid thmid ""
12.68 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
12.69 - Trueprop $ (mk_equality (t, denom)))
12.70 -
12.71 + SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
12.72 + Trueprop $ (mk_equality (t, denom)))
12.73 | eval_get_denominator _ _ _ _ = NONE;
12.74
12.75 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
12.76 fun eval_get_numerator (thmid:string) _
12.77 - (t as Const ("Rational.get_numerator", _) $
12.78 - (Const ("Fields.inverse_class.divide", _) $num
12.79 - $denom )) thy =
12.80 - SOME (mk_thmid thmid ""
12.81 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) num) "",
12.82 - Trueprop $ (mk_equality (t, num)))
12.83 + (t as Const ("Rational.get_numerator", _) $
12.84 + (Const ("Fields.inverse_class.divide", _) $num
12.85 + $denom )) thy =
12.86 + SOME (mk_thmid thmid "" (term_to_string''' thy num) "",
12.87 + Trueprop $ (mk_equality (t, num)))
12.88 | eval_get_numerator _ _ _ _ = NONE;
12.89
12.90 -
12.91 (*-------------------18.3.03 --> struct <-----------vvv--*)
12.92 val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
12.93
13.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Jul 21 15:15:50 2013 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Jul 22 13:52:18 2013 +0200
13.3 @@ -176,43 +176,37 @@
13.4 (** evaluation of numerals and predicates **)
13.5
13.6 (*does a term contain a root ? WN110518 seems incorrect, compare contains_root*)
13.7 -fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy =
13.8 +fun eval_root_free (thmid:string) _ (t as (Const (op0, t0) $ arg)) thy =
13.9 if strip_thy op0 <> "is'_root'_free"
13.10 - then error ("eval_root_free: wrong "^op0)
13.11 + then error ("eval_root_free: wrong " ^ op0)
13.12 else if const_in (strip_thy op0) arg
13.13 - then SOME (mk_thmid thmid ""
13.14 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) arg)"",
13.15 - Trueprop $ (mk_equality (t, @{term False})))
13.16 - else SOME (mk_thmid thmid ""
13.17 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) arg)"",
13.18 - Trueprop $ (mk_equality (t, @{term True})))
13.19 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
13.20 + Trueprop $ (mk_equality (t, @{term False})))
13.21 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
13.22 + Trueprop $ (mk_equality (t, @{term True})))
13.23 | eval_root_free _ _ _ _ = NONE;
13.24
13.25 (*does a term contain a root ?*)
13.26 fun eval_contains_root (thmid:string) _
13.27 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
13.28 if member op = (ids_of arg) "sqrt"
13.29 - then SOME (mk_thmid thmid ""
13.30 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) arg)"",
13.31 - Trueprop $ (mk_equality (t, @{term True})))
13.32 - else SOME (mk_thmid thmid ""
13.33 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) arg)"",
13.34 - Trueprop $ (mk_equality (t, @{term False})))
13.35 + then SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
13.36 + Trueprop $ (mk_equality (t, @{term True})))
13.37 + else SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
13.38 + Trueprop $ (mk_equality (t, @{term False})))
13.39 | eval_contains_root _ _ _ _ = NONE;
13.40
13.41 (*dummy precondition for root-met of x+1=2*)
13.42 fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
13.43 - SOME (mk_thmid thmid ""
13.44 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) (arg))"",
13.45 - Trueprop $ (mk_equality (t, @{term True})))
13.46 -| eval_precond_rootmet _ _ _ _ = NONE;
13.47 + SOME (mk_thmid thmid "" (term_to_string''' thy arg)"",
13.48 + Trueprop $ (mk_equality (t, @{term True})))
13.49 + | eval_precond_rootmet _ _ _ _ = NONE;
13.50
13.51 (*dummy precondition for root-pbl of x+1=2*)
13.52 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
13.53 - SOME (mk_thmid thmid ""
13.54 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) (arg)) "",
13.55 - Trueprop $ (mk_equality (t, @{term True})))
13.56 -| eval_precond_rootpbl _ _ _ _ = NONE;
13.57 + SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
13.58 + Trueprop $ (mk_equality (t, @{term True})))
13.59 + | eval_precond_rootpbl _ _ _ _ = NONE;
13.60
13.61 calclist':= overwritel (!calclist',
13.62 [("is_root_free", ("Test.is'_root'_free",
14.1 --- a/src/Tools/isac/ProgLang/Tools.thy Sun Jul 21 15:15:50 2013 +0200
14.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Mon Jul 22 13:52:18 2013 +0200
14.3 @@ -91,14 +91,16 @@
14.4 (*. evaluate the predicate matches (match on whole term only) .*)
14.5 (*("matches",("Tools.matches",eval_matches "#matches_")):calc*)
14.6 fun eval_matches (thmid:string) "Tools.matches"
14.7 - (t as Const ("Tools.matches",_) $ pat $ tst) thy =
14.8 + (t as Const ("Tools.matches",_) $ pat $ tst) thy =
14.9 if matches thy tst pat
14.10 - then let val prop = Trueprop $ (mk_equality (t, @{term True}))
14.11 - in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
14.12 - prop, prop) end
14.13 - else let val prop = Trueprop $ (mk_equality (t, @{term False}))
14.14 - in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
14.15 - prop, prop) end
14.16 + then
14.17 + let
14.18 + val prop = Trueprop $ (mk_equality (t, @{term True}))
14.19 + in SOME (term_to_string''' thy prop, prop) end
14.20 + else
14.21 + let
14.22 + val prop = Trueprop $ (mk_equality (t, @{term False}))
14.23 + in SOME (term_to_string''' thy prop, prop) end
14.24 | eval_matches _ _ _ _ = NONE;
14.25 (*
14.26 > val t = (term_of o the o (parse thy))
14.27 @@ -169,25 +171,23 @@
14.28
14.29 (*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)
14.30 fun eval_matchsub (thmid:string) "Tools.matchsub"
14.31 - (t as Const ("Tools.matchsub",_) $ pat $ tst) thy =
14.32 + (t as Const ("Tools.matchsub",_) $ pat $ tst) thy =
14.33 if matchsub thy tst pat
14.34 - then let val prop = Trueprop $ (mk_equality (t, @{term True}))
14.35 - in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
14.36 - prop, prop) end
14.37 - else let val prop = Trueprop $ (mk_equality (t, @{term False}))
14.38 - in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
14.39 - prop, prop) end
14.40 + then
14.41 + let val prop = Trueprop $ (mk_equality (t, @{term True}))
14.42 + in SOME (term_to_string''' thy prop, prop) end
14.43 + else
14.44 + let val prop = Trueprop $ (mk_equality (t, @{term False}))
14.45 + in SOME (term_to_string''' thy prop, prop) end
14.46 | eval_matchsub _ _ _ _ = NONE;
14.47
14.48 (*get the variables in an isabelle-term*)
14.49 (*("Vars" ,("Tools.Vars" ,eval_var "#Vars_")):calc*)
14.50 -fun eval_var (thmid:string) "Tools.Vars"
14.51 - (t as (Const(op0,t0) $ arg)) thy =
14.52 - let
14.53 - val t' = ((list2isalist HOLogic.realT) o vars) t;
14.54 - val thmId = thmid ^ (Print_Mode.setmp [] (Syntax.string_of_term
14.55 - (thy2ctxt thy)) arg);
14.56 - in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
14.57 +fun eval_var (thmid:string) "Tools.Vars" (t as (Const(op0,t0) $ arg)) thy =
14.58 + let
14.59 + val t' = ((list2isalist HOLogic.realT) o vars) t;
14.60 + val thmId = thmid ^ term_to_string''' thy arg;
14.61 + in SOME (thmId, Trueprop $ (mk_equality (t, t'))) end
14.62 | eval_var _ _ _ _ = NONE;
14.63
14.64 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
15.1 --- a/src/Tools/isac/calcelems.sml Sun Jul 21 15:15:50 2013 +0200
15.2 +++ b/src/Tools/isac/calcelems.sml Mon Jul 22 13:52:18 2013 +0200
15.3 @@ -634,11 +634,21 @@
15.4 *)
15.5 end;
15.6
15.7 -fun term2str t =
15.8 +fun term_to_string' ctxt t =
15.9 let
15.10 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory "Isac"));
15.11 + val ctxt' = Config.put show_markup false ctxt
15.12 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
15.13 +fun term_to_string'' (thyID : thyID) t =
15.14 + let
15.15 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
15.16 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
15.17 +fun term_to_string''' thy t =
15.18 + let
15.19 + val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
15.20 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
15.21
15.22 +fun term_to_string t = term_to_string'' "Isac" t;
15.23 +fun term2str t = term_to_string'' "Isac" t; (*legacy*)
15.24 fun terms2str ts = (strs2str o (map term2str )) ts;
15.25 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
15.26 fun terms2str' ts = (strs2str' o (map term2str )) ts;
15.27 @@ -649,12 +659,23 @@
15.28 fun termopt2str (SOME t) = "SOME " ^ term2str t
15.29 | termopt2str NONE = "NONE";
15.30
15.31 -fun type2str typ =
15.32 - Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
15.33 -val string_of_typ = type2str;
15.34 -fun string_of_typ_thy thy typ =
15.35 - Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt thy)) typ;
15.36 +fun type_to_string' ctxt t =
15.37 + let
15.38 + val ctxt' = Config.put show_markup false ctxt
15.39 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
15.40 +fun type_to_string'' (thyID : thyID) t =
15.41 + let
15.42 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
15.43 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
15.44 +fun type_to_string''' thy t =
15.45 + let
15.46 + val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
15.47 + in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
15.48
15.49 +fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
15.50 +val string_of_typ = type2str; (*legacy*)
15.51 +fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
15.52 +
15.53 fun subst2str (s:subst) =
15.54 (strs2str o
15.55 (map (linefeed o pair2str o
16.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Sun Jul 21 15:15:50 2013 +0200
16.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Jul 22 13:52:18 2013 +0200
16.3 @@ -3,12 +3,12 @@
16.4 theory example_3 imports Isac
16.5 begin
16.6
16.7 -section{*Function Decleration*}
16.8 +section{*Function Declaration*}
16.9 text{*Following code should only represent an example and was taken as a
16.10 snipset from Rationals.thy located in
16.11 \texttt{/src/Tools/isac/Knowledge}*}
16.12
16.13 -(*----START----Example Function Decleration from Rationals.thy----*)
16.14 +(*----START----Example Function Declaration from Rationals.thy----*)
16.15
16.16 text{*Define Method name and input, output types*}
16.17
16.18 @@ -26,10 +26,8 @@
16.19 (t as Const ("Rational.get_denominator", _) $
16.20 (Const ("Fields.inverse_class.divide", _) $num
16.21 $denom)) thy =
16.22 - SOME (mk_thmid thmid ""
16.23 - (Print_Mode.setmp []
16.24 - (Syntax.string_of_term (thy2ctxt thy)) denom) "",
16.25 - Trueprop $ (mk_equality (t, denom)))
16.26 + SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
16.27 + Trueprop $ (mk_equality (t, denom)))
16.28 | eval_get_denominator _ _ _ _ = NONE;
16.29 *}
16.30 (*----END----Example Function Decleration from Rationals.thy----*)
17.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Jul 21 15:15:50 2013 +0200
17.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jul 22 13:52:18 2013 +0200
17.3 @@ -218,10 +218,8 @@
17.4 (t as Const ("Rational.get_denominator", _) $
17.5 (Const ("Fields.inverse_class.divide", _) $num
17.6 $denom)) thy =
17.7 - SOME (mk_thmid thmid ""
17.8 - (Print_Mode.setmp []
17.9 - (Syntax.string_of_term (thy2ctxt thy)) denom) "",
17.10 - Trueprop $ (mk_equality (t, denom)))
17.11 + SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
17.12 + Trueprop $ (mk_equality (t, denom)))
17.13 | eval_get_denominator _ _ _ _ = NONE;
17.14 *}
17.15 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
17.16 @@ -240,10 +238,8 @@
17.17 (t as Const ("Rational.get_numerator", _) $
17.18 (Const ("Fields.inverse_class.divide", _) $num
17.19 $denom )) thy =
17.20 - SOME (mk_thmid thmid ""
17.21 - (Print_Mode.setmp []
17.22 - (Syntax.string_of_term (thy2ctxt thy)) num) "",
17.23 - Trueprop $ (mk_equality (t, num)))
17.24 + SOME (mk_thmid thmid "" (term_to_string''' thy num) "",
17.25 + Trueprop $ (mk_equality (t, num)))
17.26 | eval_get_numerator _ _ _ _ = NONE;
17.27 *}
17.28
17.29 @@ -446,9 +442,7 @@
17.30 fun eval_factors_from_solution (thmid:string) _
17.31 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
17.32 thy = ((let val prod = factors_from_solution sol
17.33 - in SOME (mk_thmid thmid ""
17.34 - (Print_Mode.setmp []
17.35 - (Syntax.string_of_term (thy2ctxt thy)) prod) "",
17.36 + in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "",
17.37 Trueprop $ (mk_equality (t, prod)))
17.38 end)
17.39 handle _ => NONE)
18.1 --- a/test/Tools/isac/Interpret/solve.sml Sun Jul 21 15:15:50 2013 +0200
18.2 +++ b/test/Tools/isac/Interpret/solve.sml Mon Jul 22 13:52:18 2013 +0200
18.3 @@ -9,6 +9,7 @@
18.4 uses from Poly.ML: Rls make_polynomial, Rls expand_binom
18.5 *)
18.6
18.7 +print_depth 5;
18.8 "-----------------------------------------------------------------";
18.9 "table of contents -----------------------------------------------";
18.10 "-----------------------------------------------------------------";
19.1 --- a/test/Tools/isac/Knowledge/atools.sml Sun Jul 21 15:15:50 2013 +0200
19.2 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Jul 22 13:52:18 2013 +0200
19.3 @@ -7,6 +7,7 @@
19.4 use"atools.sml";
19.5 *)
19.6
19.7 +print_depth 5;
19.8 "--------------------------------------------------------";
19.9 "table of contents --------------------------------------";
19.10 "--------------------------------------------------------";
19.11 @@ -27,16 +28,16 @@
19.12 "----------- occurs_in -------------------------------------------";
19.13 (*=========================================================================*)
19.14 fun str2t str = (term_of o the o (parse thy)) str;
19.15 -fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t;
19.16 +fun term2s t = term_to_string''' thy t;
19.17 (*=========================================================================*)
19.18
19.19 val t = str2t "x";
19.20 -if occurs_in t t then "OK" else error "atools.sml: occurs_in x x -> f";
19.21 +if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
19.22
19.23 -val t = str2t "x occurs_in x";
19.24 +val t = str2term "x occurs_in x";
19.25 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
19.26 -if (term2s t') = "x occurs_in x = True" then ()
19.27 -else error "atools.sml: x occurs_in x = True ???";
19.28 +if term2str t' = "x occurs_in x = True" then ()
19.29 +else error "x occurs_in x = True ..changed";
19.30
19.31 "------- some_occur_in";
19.32 some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");
19.33 @@ -57,9 +58,9 @@
19.34 "----------- argument_of -----------------------------------------";
19.35 "----------- argument_of -----------------------------------------";
19.36 "----------- argument_of -----------------------------------------";
19.37 -val t = str2t "argument_in (M_b x)";
19.38 +val t = str2term "argument_in (M_b x)";
19.39 val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
19.40 -if term2s t' = "(argument_in M_b x) = x" then ()
19.41 +if term2str t' = "(argument_in M_b x) = x" then ()
19.42 else error "atools.sml:(argument_in M_b x) = x ???";
19.43
19.44 "----------- sameFunId -------------------------------------------";
20.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Sun Jul 21 15:15:50 2013 +0200
20.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Mon Jul 22 13:52:18 2013 +0200
20.3 @@ -2,7 +2,7 @@
20.4 author: Walther Neuper 050826
20.5 (c) due to copyright terms
20.6 *)
20.7 -
20.8 +trace_rewrite := false;
20.9 "-----------------------------------------------------------------";
20.10 "table of contents -----------------------------------------------";
20.11 "-----------------------------------------------------------------";
20.12 @@ -23,7 +23,7 @@
20.13 val thy = @{theory "Biegelinie"};
20.14 val ctxt = thy2ctxt' "Biegelinie";
20.15 fun str2term str = (term_of o the o (parse thy)) str;
20.16 -fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt' "Biegelinie")) t;
20.17 +fun term2s t = term_to_string'' "Biegelinie" t;
20.18 fun rewrit thm str =
20.19 fst (the (rewrite_ thy tless_true e_rls true thm str));
20.20
20.21 @@ -91,7 +91,7 @@
20.22 if term2str x1__ = "0" then ()
20.23 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
20.24
20.25 -trace_rewrite:=true;
20.26 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
20.27 trace_rewrite:=false;
20.28
20.29 "----------- Bsp 7.27 me -----------------------------------------";
20.30 @@ -431,7 +431,6 @@
20.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.32 if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
20.33 then () else error "biegelinie.sml met2 b";
20.34 -(*=== inhibit exn 110722=============================================================*)
20.35
20.36 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
20.37 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
20.38 @@ -492,7 +491,6 @@
20.39 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]" then ()
20.40 else error "biegelinie.sml met2 e";
20.41
20.42 -
20.43 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
20.44 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
20.45 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
20.46 @@ -527,7 +525,6 @@
20.47 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
20.48 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
20.49 "----- check the scripts syntax";
20.50 -(*WN120309 deleted*)
20.51 "----- execute script by interpreter: setzeRandbedingungenEin";
20.52 val fmz = ["Funktionen [Q x = c + -1 * q_0 * x," ^
20.53 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2," ^
20.54 @@ -609,7 +606,9 @@
20.55 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
20.56 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
20.57 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.58 -case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
20.59 +(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
20.60 +
20.61 +case nxt of (_, Subproblem (_, ["makeFunctionTo", "equation"])) => ()
20.62 | _ => error "biegelinie.sml met2 ll";
20.63
20.64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.65 @@ -631,6 +630,7 @@
20.66 (* "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" *)
20.67 "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /\n (-1 * EI * 24),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
20.68 then () else error "biegelinie.sml met2 oo";
20.69 +============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
20.70
20.71 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
20.72 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
20.73 @@ -648,6 +648,7 @@
20.74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.76 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.77 +(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
20.78 if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
20.79 then () else error "biegelinie.sml met2 a";
20.80
20.81 @@ -703,11 +704,11 @@
20.82 ]
20.83 ;
20.84 val t = str2term "last [1,2,3,4]";
20.85 -trace_rewrite := true;
20.86 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
20.87 val SOME (e1__,_) = rewrite_set_ thy false srls t;
20.88 trace_rewrite := false;
20.89 term2str e1__;
20.90 -
20.91 +============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
20.92
20.93 "----------- investigate normalforms in biegelinien --------------";
20.94 "----------- investigate normalforms in biegelinien --------------";
21.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Sun Jul 21 15:15:50 2013 +0200
21.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Jul 22 13:52:18 2013 +0200
21.3 @@ -3,6 +3,7 @@
21.4 (c) due to copyright terms
21.5 *)
21.6
21.7 +trace_rewrite := false;
21.8 "-----------------------------------------------------------------";
21.9 "table of contents -----------------------------------------------";
21.10 "-----------------------------------------------------------------";
22.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sun Jul 21 15:15:50 2013 +0200
22.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Jul 22 13:52:18 2013 +0200
22.3 @@ -2,6 +2,7 @@
22.4 author: Walther Neuper 2005
22.5 (c) due to copyright terms
22.6 *)
22.7 +trace_rewrite := false;
22.8 "--------------------------------------------------------";
22.9 "table of contents --------------------------------------";
22.10 "--------------------------------------------------------";
22.11 @@ -31,7 +32,7 @@
22.12 val ctxt = thy2ctxt thy;
22.13
22.14 fun str2t str = parseNEW ctxt str |> the;
22.15 -fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term ctxt) t;
22.16 +fun term2s t = term_to_string' ctxt t;
22.17
22.18 val conditions_in_integration_rules =
22.19 Rls {id="conditions_in_integration_rules",
23.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Sun Jul 21 15:15:50 2013 +0200
23.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 22 13:52:18 2013 +0200
23.3 @@ -2,9 +2,6 @@
23.4 author: Walther Neuper
23.5 WN071207,
23.6 (c) due to copyright terms
23.7 -
23.8 -use"../smltest/IsacKnowledge/polyminus.sml";
23.9 -use"polyminus.sml";
23.10 *)
23.11 "--------------------------------------------------------";
23.12 "--------------------------------------------------------";
23.13 @@ -69,7 +66,7 @@
23.14 "----------- watch order_add_mult -------------------------------";
23.15 "----------- watch order_add_mult -------------------------------";
23.16 "----- with these simple variables it works...";
23.17 -trace_rewrite:=true;
23.18 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
23.19 trace_rewrite:=false;
23.20 val t = str2term "((a + d) + c) + b";
23.21 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
23.22 @@ -172,7 +169,7 @@
23.23 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t;
23.24
23.25 "======= test rewrite_, rewrite_set_";
23.26 -trace_rewrite:=true;
23.27 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
23.28 val erls = erls_ordne_alphabetisch;
23.29 val t = str2term "b + a";
23.30 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
23.31 @@ -230,7 +227,7 @@
23.32 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()
23.33 else error "polyminus.sml: verschoenere 3 + -2 * e ...";
23.34
23.35 -trace_rewrite:=true;
23.36 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
23.37 trace_rewrite:=false;
23.38
23.39 "----------- met simplification for_polynomials with_minus -------";
23.40 @@ -422,7 +419,7 @@
23.41 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
23.42 val ((pt,p),_) = get_calc 1; show_pt pt;
23.43 "----- 2 ^^^";
23.44 -trace_rewrite := true;
23.45 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
23.46 val erls = erls_ordne_alphabetisch;
23.47 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
23.48 val SOME (t',_) =
23.49 @@ -579,7 +576,7 @@
23.50 (*"(~ True) = False"*)
23.51 Thm ("not_false",num_str @{thm not_false})
23.52 (*"(~ False) = True"*)];
23.53 -trace_rewrite := true;
23.54 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
23.55 val SOME (t', _) = rewrite_set_ thy false prls t;
23.56 trace_rewrite := false;
23.57
23.58 @@ -589,7 +586,7 @@
23.59 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
23.60 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
23.61 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
23.62 -trace_rewrite := true;
23.63 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
23.64 val SOME (t', _) = rewrite_set_ thy false prls t;
23.65 trace_rewrite := false;
23.66 if term2str t' = "False" then ()
24.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Sun Jul 21 15:15:50 2013 +0200
24.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Mon Jul 22 13:52:18 2013 +0200
24.3 @@ -8,8 +8,89 @@
24.4 ("Test", ["sqroot-test","univariate","equation","test"],
24.5 ["Test","squ-equ-test-subpbl1"]);
24.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*)
24.7 +(*for resuming after stepping into code*)
24.8 +val (p''',f''',nxt''',pt''') = (p,f,nxt,pt);
24.9 +
24.10 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ptree)) = (nxt, p, [], pt);
24.11 + val (pt, p) =
24.12 + case locatetac tac (pt,p) of
24.13 + ("ok", (_, _, ptp)) => ptp;
24.14 +(* val (_, ts) =
24.15 + (case step p ((pt, e_pos'),[]) of
24.16 + ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts))
24.17 +ERROR: ts = [(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'", ...*)
24.18 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
24.19 + (p, ((pt, e_pos'),[]));
24.20 + val pIopt = get_pblID (pt,ip);
24.21 +ip = ([],Res); (* = false*)
24.22 +tacis; (* = []*)
24.23 +pIopt; (* = SOME ["sqroot-test", "univariate", "equation", "test"]*)
24.24 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = true*)
24.25 +
24.26 +(* nxt_specify_ (pt, ip)
24.27 +ERROR: = ([(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'",...*)
24.28 +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);
24.29 +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
24.30 + probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
24.31 +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*)
24.32 + val cpI = if pI = e_pblID then pI' else pI;
24.33 + val cmI = if mI = e_metID then mI' else mI;
24.34 + val {ppc, prls, where_, ...} = get_pbt cpI;
24.35 + val pre = check_preconds "thy 100820" prls where_ probl;
24.36 + val pb = foldl and_ (true, map fst pre);
24.37 +
24.38 +(* val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
24.39 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
24.40 +ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
24.41 +"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : spec),
24.42 + ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : spec)) =
24.43 + (p_, pb, oris, (dI',pI',mI'), (probl, meth),
24.44 + (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
24.45 +
24.46 +dI' = e_domID andalso dI = e_domID; (* = false*)
24.47 +pI' = e_pblID andalso pI = e_pblID; (* = false*)
24.48 +find_first (is_error o #5) (pbl:itm list); (* = NONE*)
24.49 +
24.50 +(* nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl;
24.51 += SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
24.52 +"~~~~~ fun nxt_add, args:"; val (thy, oris, pbt, itms) =
24.53 + ((assoc_thy (if dI = e_domID then dI' else dI)), oris, pbt, pbl);
24.54 +local infix mem;
24.55 +fun x mem [] = false
24.56 + | x mem (y :: ys) = x = y orelse x mem ys;
24.57 +in
24.58 + fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
24.59 + andalso (#3 ori) <>"#undef";
24.60 + fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
24.61 + fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
24.62 + fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
24.63 + (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
24.64 + fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
24.65 + | false_and_not_Sup (i,v,false,f, _) = true
24.66 + | false_and_not_Sup _ = false;
24.67 +end
24.68 + val v = if itms = [] then 1 else max_vt itms;
24.69 + val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
24.70 + val vits = if v = 0 then itms (*because of dsc without dat*)
24.71 + else filter (testi_vt v) itms; (*itms..vat*)
24.72 + val icl = filter false_and_not_Sup vits; (* incomplete *)
24.73 +icl = []; (* = false*)
24.74 +val SOME ori = find_first (test_subset (hd icl)) vors;
24.75 +
24.76 +(* SOME (geti_ct thy ori (hd icl))
24.77 +ERROR: SOME (geti_ct thy ori (hd icl))*)
24.78 +"~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : ori), ((_, _, _, fd, itm_) : itm)) =
24.79 + (thy, ori, (hd icl));
24.80 +"~~~~~ to return val:"; val xxx =
24.81 + ( fd,
24.82 + ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm'
24.83 + );
24.84 +if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";
24.85 +
24.86 +(* resuming after stepping into code*)
24.87 +val (p,f,nxt,pt) = (p''',f''',nxt''',pt''');
24.88 +
24.89 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*)
24.90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*)
24.91 case nxt of (_, Add_Given "solveFor x") => ()
24.92 | _ => error "minisubpbl: Add_Given is broken in root-problem";
24.93 -
25.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sun Jul 21 15:15:50 2013 +0200
25.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Mon Jul 22 13:52:18 2013 +0200
25.3 @@ -194,7 +194,7 @@
25.4 "----------- check calculate bottom up ------------------";
25.5 "----------- check calculate bottom up ------------------";
25.6 (*-------------- eval_cancel works: *)
25.7 - trace_rewrite:=true;
25.8 + trace_rewrite:=false;
25.9 val thy = @{theory Test};
25.10 val t = (term_of o the o (parse thy)) "(-4) / 2";
25.11
25.12 @@ -226,7 +226,7 @@
25.13 val (t,_) = the (rewrite_set thy false rls t);
25.14 (*val t = "2 + x" ... works*)
25.15
25.16 - trace_rewrite:=true; (*3.6.03*)
25.17 + trace_rewrite:=false; (*=true3.6.03*)
25.18
25.19 val thy = "Test";
25.20 val rls = "Test_simplify";
25.21 @@ -235,7 +235,7 @@
25.22 (*val t = "2 + x" ... works: give up----------------------------------------*)
25.23 trace_rewrite:=false;
25.24
25.25 - trace_rewrite:=true; (*3.6.03*)
25.26 + trace_rewrite:=false; (*=true3.6.03*)
25.27 val thy = @{theory Test};
25.28 val rls = Test_simplify;
25.29 val t = str2term "(3+(1+2*x))/2";
25.30 @@ -276,7 +276,7 @@
25.31
25.32
25.33 (*===================*)
25.34 - trace_rewrite:=true;
25.35 + trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
25.36 val thy' = "Test";
25.37 val rls = "Test_simplify";
25.38 val ct = "x + (-1 + -3) / 2";
25.39 @@ -295,7 +295,7 @@
25.40 ### trying calc. 'pow'
25.41 *)
25.42
25.43 - trace_rewrite:=true;
25.44 + trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
25.45 val thy' = "Test";
25.46 val rls = "Test_simplify";
25.47 val ct = "x + (-4) / 2";
26.1 --- a/test/Tools/isac/ProgLang/termC.sml Sun Jul 21 15:15:50 2013 +0200
26.2 +++ b/test/Tools/isac/ProgLang/termC.sml Mon Jul 22 13:52:18 2013 +0200
26.3 @@ -423,7 +423,7 @@
26.4 |-> Proof_Context.read_term_pattern
26.5 |> numbers_to_string;
26.6 val t_real = typ_a2real t;
26.7 -if Print_Mode.setmp [] (Syntax.string_of_term ctxt) t_real =
26.8 +if term_to_string' ctxt t_real =
26.9 "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c))" ^
26.10 " t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" then ()
26.11 else error "";
26.12 @@ -434,8 +434,7 @@
26.13 val t = @{term "x + 1"};
26.14 val str_markup = (Syntax.string_of_term
26.15 (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
26.16 - val str = Print_Mode.setmp [] (Syntax.string_of_term
26.17 - (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
26.18 + val str = term_to_string'' "Isac" t;
26.19
26.20 writeln "----------------writeln str_markup---";
26.21 writeln str_markup;
26.22 @@ -473,8 +472,7 @@
26.23 val t = @{term "x + 1"};
26.24 val str_markup = (Syntax.string_of_term
26.25 (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
26.26 - val str = Print_Mode.setmp [] (Syntax.string_of_term
26.27 - (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;
26.28 + val str = term_to_string'' "Isac" t;
26.29
26.30 writeln "----------------writeln str_markup---";
26.31 writeln str_markup;
27.1 --- a/test/Tools/isac/Test_Some.thy Sun Jul 21 15:15:50 2013 +0200
27.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 22 13:52:18 2013 +0200
27.3 @@ -1,6 +1,7 @@
27.4
27.5 theory Test_Some imports Isac begin
27.6 - ML_file "ProgLang/calculate.sml"
27.7 + ML_file "calcelems.sml"
27.8 +(*ML_file "Knowledge/biegelinie.sml"*)
27.9 (*
27.10 declare [[show_types]]
27.11 declare [[show_sorts]]
27.12 @@ -21,20 +22,12 @@
27.13 *}
27.14 ML {*
27.15 *}
27.16 -ML {*
27.17 -*}
27.18 -ML {*
27.19 -*}
27.20 ML {* (*==================*)
27.21 *}
27.22 ML {*
27.23 *}
27.24 ML {*
27.25 *}
27.26 -ML {*
27.27 -*}
27.28 -ML {*
27.29 -*}
27.30 ML {* (*==================*)
27.31 "~~~~~ fun , args:"; val () = ();
27.32
27.33 @@ -45,8 +38,8 @@
27.34
27.35 (*========== inhibit exn WN1130701 broken already in 2009-2 =======================
27.36 ============ inhibit exn WN1130701 broken already in 2009-2 =====================*)
27.37 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
27.38 -============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
27.39 +(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
27.40 +============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
27.41
27.42 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
27.43 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
28.1 --- a/test/Tools/isac/library.sml Sun Jul 21 15:15:50 2013 +0200
28.2 +++ b/test/Tools/isac/library.sml Mon Jul 22 13:52:18 2013 +0200
28.3 @@ -1,7 +1,6 @@
28.4 Toplevel.debug := true;
28.5
28.6 -fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
28.7 -(Proof_Context.init_global (Thy_Info.get_theory "Rational"))) t;
28.8 +fun term2st t = term_to_string'' "Rational" t;
28.9 (*..............................................########......................*)
28.10
28.11 "--- Pure/General/ord_list.ML";