intermed. test/../integrate.sml in -- me method [diff,integration] --
removed last error by
find . -type f -exec sed -i s/"\"Isac.thy\""/"\"Isac\""/g {} \;
find . -type f -exec sed -i s/" Isac.thy"/" (theory \"Isac\")"/g {} \;
1.1 --- a/src/Tools/isac/Frontend/interface.sml Wed Oct 06 14:52:12 2010 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Oct 06 15:12:41 2010 +0200
1.3 @@ -449,7 +449,7 @@
1.4 Notappl e => message2xml cI ("'" ^ tac2str tac ^
1.5 "' not-applicable")
1.6 | Appl m =>
1.7 - let val (p,c,_,pt) = generate1 (assoc_thy"Isac.thy")
1.8 + let val (p,c,_,pt) = generate1 (assoc_thy"Isac")
1.9 m Uistate ip pt
1.10 in upd_calc cI ((pt,p),[]);
1.11 autocalculateOK2xml cI pold (if null c then pold
2.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Oct 06 14:52:12 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Wed Oct 06 15:12:41 2010 +0200
2.3 @@ -165,12 +165,12 @@
2.4 (*before 5.03-----
2.5 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
2.6 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
2.7 -> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
2.8 +> val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
2.9 val ct' = "True" : cterm'
2.10
2.11 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
2.12 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
2.13 -> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
2.14 +> val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
2.15 val ct' = "True" : cterm'
2.16
2.17
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Oct 06 14:52:12 2010 +0200
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Oct 06 15:12:41 2010 +0200
3.3 @@ -1296,7 +1296,7 @@
3.4 Model_Problem, Safe, pt) end
3.5
3.6 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
3.7 - let val (pos,_,_,pt) = generate1 (assoc_thy "Isac.thy")
3.8 + let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
3.9 (Refine_Problem' rfd) Uistate pos pt
3.10 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
3.11 Model_Problem, Safe, pt) end
3.12 @@ -1629,7 +1629,7 @@
3.13 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
3.14 let val (dI',_,_) = get_obj g_spec pt p
3.15 val (pos,c,_,pt) =
3.16 - generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI)
3.17 + generate1 (assoc_thy "Isac") (Specify_Theory' dI)
3.18 Uistate pos pt
3.19 in (*FIXXXME: check if pbl can still be parsed*)
3.20 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
3.21 @@ -1638,7 +1638,7 @@
3.22 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
3.23 let val (dI',_,_) = get_obj g_spec pt p
3.24 val (pos,c,_,pt) =
3.25 - generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI)
3.26 + generate1 (assoc_thy "Isac") (Specify_Theory' dI)
3.27 Uistate pos pt
3.28 in (*FIXXXME: check if met can still be parsed*)
3.29 ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
3.30 @@ -1678,7 +1678,7 @@
3.31 in ((pt,([],Pbl)), []): calcstate end
3.32 else if mI <> [] then (*comes from met-browser*)
3.33 let val {ppc,...} = get_met mI
3.34 - val dI = if dI = "" then "Isac.thy" else dI
3.35 + val dI = if dI = "" then "Isac" else dI
3.36 val thy = assoc_thy dI
3.37 val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
3.38 ([], (dI,pI,mI), e_term(*FIXME met*))
3.39 @@ -2169,14 +2169,14 @@
3.40 let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
3.41 get_obj I pt p
3.42 val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
3.43 - val pre = check_preconds (assoc_thy"Isac.thy") prls where_ probl
3.44 + val pre = check_preconds (assoc_thy"Isac") prls where_ probl
3.45 in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
3.46 | get_ocalhd (pt, pos' as (p,Met):pos') =
3.47 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
3.48 spec, meth,...} =
3.49 get_obj I pt p
3.50 val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
3.51 - val pre = check_preconds (assoc_thy"Isac.thy") prls pre meth
3.52 + val pre = check_preconds (assoc_thy"Isac") prls pre meth
3.53 in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
3.54
3.55 (*.at the activeFormula set the Model, the Guard and the Specification
4.1 --- a/src/Tools/isac/Interpret/ctree.sml Wed Oct 06 14:52:12 2010 +0200
4.2 +++ b/src/Tools/isac/Interpret/ctree.sml Wed Oct 06 15:12:41 2010 +0200
4.3 @@ -503,16 +503,16 @@
4.4 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
4.5
4.6 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
4.7 - (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
4.8 + (thmID, SOME ((subs2subst (assoc_thy "Isac") subs):subst))
4.9 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
4.10 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
4.11
4.12 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
4.13 - (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst))
4.14 + (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst))
4.15 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
4.16 | rls_of_rewset (Detail_Set rls) = (rls, NONE)
4.17 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
4.18 - (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst));
4.19 + (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst));
4.20
4.21 fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)
4.22 | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
5.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Oct 06 14:52:12 2010 +0200
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Oct 06 15:12:41 2010 +0200
5.3 @@ -26,7 +26,7 @@
5.4 | init_istate (Rewrite_Set_Inst (subs, rls)) =
5.5 (* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
5.6 *)
5.7 - let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
5.8 + let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
5.9 in case assoc_rls rls of
5.10 Rls {scr=EmptyScr,...} =>
5.11 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
5.12 @@ -67,7 +67,7 @@
5.13 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
5.14 *)
5.15 | init_istate (Rewrite_Set_Inst (subs, rls)) t =
5.16 - let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
5.17 + let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
5.18 (*...we suppose the substitution of only _one_ bound variable*)
5.19 in case assoc_rls rls of
5.20 Rls {scr=EmptyScr,...} =>
5.21 @@ -330,7 +330,7 @@
5.22 | NONE =>
5.23 (pos,[],EmptyMout,update_env pt p (SOME is)))
5.24 (* val (thy, (Take' t), l, (p,p_), pt) =
5.25 - ((assoc_thy "Isac.thy"), tac_, is, pos, pt);
5.26 + ((assoc_thy "Isac"), tac_, is, pos, pt);
5.27 *)
5.28 | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
5.29 let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
5.30 @@ -343,7 +343,7 @@
5.31 (* val (l, (p,p_)) = (RrlsState is, p);
5.32
5.33 val (thy, Begin_Trans' t, l, (p,Frm), pt) =
5.34 - (assoc_thy "Isac.thy", tac_, is, p, pt);
5.35 + (assoc_thy "Isac", tac_, is, p, pt);
5.36 *)
5.37 | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
5.38 let (* print_depth 99;
5.39 @@ -361,7 +361,7 @@
5.40 term2str t)), pt) end
5.41
5.42 (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
5.43 - (assoc_thy "Isac.thy", tac_, is, p, pt);
5.44 + (assoc_thy "Isac", tac_, is, p, pt);
5.45 *)
5.46 | generate1 thy (Begin_Trans' t) l (p ,Res) pt =
5.47 (*append after existing PrfObj _________*)
5.48 @@ -395,7 +395,7 @@
5.49
5.50 | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
5.51 (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
5.52 - (assoc_thy "Isac.thy", tac_, is, pos, pt);
5.53 + (assoc_thy "Isac", tac_, is, pos, pt);
5.54 *)
5.55 let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
5.56 val (pt,c) = cappend_atomic pt p l f
5.57 @@ -505,7 +505,7 @@
5.58 (* for recursion ...
5.59 (tacis', (_, tac_, (p, is))) = split_last tacis';
5.60 *)
5.61 - val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt
5.62 + val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
5.63 in generate tacis' (pt', c@c', p') end;
5.64
5.65
6.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Oct 06 14:52:12 2010 +0200
6.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Oct 06 15:12:41 2010 +0200
6.3 @@ -219,8 +219,8 @@
6.4 in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end
6.5 end;
6.6
6.7 -(*lazy evaluation for Isac.thy*)
6.8 -fun Isac _ = assoc_thy "Isac.thy";
6.9 +(*lazy evaluation for (theory "Isac")*)
6.10 +fun Isac _ = assoc_thy "Isac";
6.11
6.12 (*re-parse itms with a new thy and prepare for checking with ori list*)
6.13 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
6.14 @@ -453,7 +453,7 @@
6.15 let val pbt = (#ppc o get_pbt) pI
6.16 val dI' = #1 (some_spec ospec spec)
6.17 val oris = if pI = #2 ospec then oris
6.18 - else prep_ori fmz_(assoc_thy"Isac.thy") pbt;
6.19 + else prep_ori fmz_(assoc_thy"Isac") pbt;
6.20 in (Pbl, appl_adds dI' oris probl pbt
6.21 (map itms2fstr probl), meth) end else
6.22 if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
6.23 @@ -468,12 +468,12 @@
6.24 val pt = update_spec pt p spec;
6.25 in if pos_ = Pbl
6.26 then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
6.27 - val pre =check_preconds(assoc_thy"Isac.thy")prls where_ pits
6.28 + val pre =check_preconds(assoc_thy"Isac")prls where_ pits
6.29 in (update_pbl pt p pits,
6.30 (ocalhd_complete pits pre spec,
6.31 Pbl, hdf', pits, pre, spec):ocalhd) end
6.32 else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
6.33 - val pre = check_preconds (assoc_thy"Isac.thy") prls pre mits
6.34 + val pre = check_preconds (assoc_thy"Isac") prls pre mits
6.35 in (update_met pt p mits,
6.36 (ocalhd_complete mits pre spec,
6.37 Met, hdf', mits, pre, spec):ocalhd) end
6.38 @@ -596,12 +596,12 @@
6.39
6.40 fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
6.41 (Rewrite (rule2thm' r),
6.42 - Rewrite' ("Isac.thy", fst ro, erls, false,
6.43 + Rewrite' ("Isac", fst ro, erls, false,
6.44 rule2thm' r, t, (t', a)),
6.45 (e_pos'(*to be updated before generate tacis!!!*), Uistate))
6.46 | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
6.47 (Rewrite_Set (rule2rls' r),
6.48 - Rewrite_Set' ("Isac.thy", false, rls, t, (t', a)),
6.49 + Rewrite_Set' ("Isac", false, rls, t, (t', a)),
6.50 (e_pos'(*to be updated before generate tacis!!!*), Uistate));
6.51
6.52 (*fo = ifo excluded already in inform*)
6.53 @@ -705,8 +705,8 @@
6.54 (([],[],(pt,p)), (encode ifo));
6.55 *)
6.56 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
6.57 - case parse (assoc_thy "Isac.thy") istr of
6.58 -(* val SOME ifo = parse (assoc_thy "Isac.thy") istr;
6.59 + case parse (assoc_thy "Isac") istr of
6.60 +(* val SOME ifo = parse (assoc_thy "Isac") istr;
6.61 *)
6.62 SOME ifo =>
6.63 let val ifo = term_of ifo
7.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Oct 06 14:52:12 2010 +0200
7.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Oct 06 15:12:41 2010 +0200
7.3 @@ -347,7 +347,7 @@
7.4 val spec = (dI',pblID,mI')
7.5 val {ppc,where_,prls,...} = get_pbt pblID
7.6 val (model_ok, (pbl, pre)) =
7.7 - match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
7.8 + match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
7.9 in ModSpec (ocalhd_complete pbl pre spec,
7.10 Pbl, e_term, pbl, pre, spec) end;*)
7.11 fun initcontext_pbl pt (pos as (p,_):pos') =
7.12 @@ -359,7 +359,7 @@
7.13 else pI'
7.14 val {ppc,where_,prls,...} = get_pbt pblID
7.15 val (model_ok, (pbl, pre)) =
7.16 - match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
7.17 + match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
7.18 in (model_ok, pblID, hdl, pbl, pre) end;
7.19
7.20 fun initcontext_met pt (pos as (p,_):pos') =
7.21 @@ -371,7 +371,7 @@
7.22 else mI'
7.23 val {ppc,pre,prls,scr,...} = get_met metID
7.24 val (model_ok, (pbl, pre)) =
7.25 - match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os
7.26 + match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
7.27 in (model_ok, metID, scr, pbl, pre) end;
7.28
7.29 (*.match the model of a problem at pos p
7.30 @@ -380,14 +380,14 @@
7.31 let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
7.32 val {ppc,where_,prls,...} = get_pbt pI
7.33 val (model_ok, (pbl, pre)) =
7.34 - match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
7.35 + match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
7.36 in (model_ok, pI, hdl, pbl, pre) end;
7.37
7.38 fun context_met mI pt (p:pos) =
7.39 let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
7.40 val {ppc,pre,prls,scr,...} = get_met mI
7.41 val (model_ok, (pbl, pre)) =
7.42 - match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os
7.43 + match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
7.44 in (model_ok, mI, scr, pbl, pre) end
7.45
7.46
7.47 @@ -395,10 +395,10 @@
7.48 *)
7.49 fun tryrefine pI pt (pos as (p,_):pos') =
7.50 let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
7.51 - in case refine_pbl (assoc_thy "Isac.thy") pI probl of
7.52 + in case refine_pbl (assoc_thy "Isac") pI probl of
7.53 NONE => (*copy from context_pbl*)
7.54 let val {ppc,where_,prls,...} = get_pbt pI
7.55 - val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy")
7.56 + val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac")
7.57 probl (ppc,where_,prls) os
7.58 in (false, pI, hdl, pbl, pre) end
7.59 | SOME (pI, (pbl, pre)) =>
7.60 @@ -437,7 +437,7 @@
7.61 | ModSpec (_,p_, head, gfr, pre, _) =>
7.62 Form' (PpcKF (0,EdUndef,0,Nundef,
7.63 (case p_ of Pbl => Problem[] | Met => Method[],
7.64 - itms2itemppc (assoc_thy"Isac.thy") gfr pre)))
7.65 + itms2itemppc (assoc_thy"Isac") gfr pre)))
7.66 end;
7.67
7.68 (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
8.1 --- a/src/Tools/isac/Interpret/mstools.sml Wed Oct 06 14:52:12 2010 +0200
8.2 +++ b/src/Tools/isac/Interpret/mstools.sml Wed Oct 06 15:12:41 2010 +0200
8.3 @@ -197,16 +197,16 @@
8.4 (*.revert split_.
8.5 WN050903 we do NOT know which is from subtheory, description or term;
8.6 typecheck thus may lead to TYPE-error 'unknown constant';
8.7 - solution: typecheck with Isac.thy; i.e. arg 'thy' superfluous*)
8.8 + solution: typecheck with (theory "Isac"); i.e. arg 'thy' superfluous*)
8.9 (*fun comp_dts thy (d,[]) =
8.10 - cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
8.11 + cterm_of (*(sign_of o assoc_thy) "Isac"*)
8.12 (theory "Isac")
8.13 (*comp_dts:FIXXME stay with term for efficiency !!!*)
8.14 (if is_reall_dsc d then (d $ e_listReal)
8.15 else if is_booll_dsc d then (d $ e_listBool)
8.16 else d)
8.17 | comp_dts thy (d,ts) =
8.18 - (cterm_of (*(sign_of o assoc_thy) "Isac.thy"*)
8.19 + (cterm_of (*(sign_of o assoc_thy) "Isac"*)
8.20 (theory "Isac")
8.21 (*comp_dts:FIXXME stay with term for efficiency !!*)
8.22 (d $ (comp_ts (d, ts)))
8.23 @@ -940,7 +940,7 @@
8.24 (* val (prls, pre) = (prls, hd pres');
8.25 val (prls, pre) = (prls, hd (tl pres'));
8.26 *)
8.27 - if eval_true (assoc_thy "Isac.thy") (*for Pattern.match *)
8.28 + if eval_true (assoc_thy "Isac") (*for Pattern.match *)
8.29 [pre] prls (*pre parsed, prls.thy*)
8.30 then (true , pre)
8.31 else (false , pre);
9.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Oct 06 14:52:12 2010 +0200
9.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Oct 06 15:12:41 2010 +0200
9.3 @@ -407,7 +407,7 @@
9.4 *)
9.5 fun thy_contains_thm (str:xstring) (_, thy) =
9.6 member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str;
9.7 -(* val (thy', str) = ("Isac.thy", "real_mult_minus1");
9.8 +(* val (thy', str) = ("Isac", "real_mult_minus1");
9.9 val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
9.10 *)
9.11 fun thy_containing_thm (thy':theory') (str:xstring) =
10.1 --- a/src/Tools/isac/Interpret/script.sml Wed Oct 06 14:52:12 2010 +0200
10.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Oct 06 15:12:41 2010 +0200
10.3 @@ -378,8 +378,8 @@
10.4 = (assoc_thy th,stac);
10.5 stac2tac_ pt thy mm;
10.6
10.7 - assoc_thm' (assoc_thy "Isac.thy") (tid,"");
10.8 - assoc_thm' Isac.thy (tid,"");
10.9 + assoc_thm' (assoc_thy "Isac") (tid,"");
10.10 + assoc_thm' (theory "Isac") (tid,"");
10.11 *)
10.12 | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $
10.13 sub $ Free (thmID,_) $ _ $ f) =
10.14 @@ -1127,7 +1127,7 @@
10.15 assy ya ((E,(l@[R]),a,v,S,b),ss) e2
10.16 | ay => (ay))
10.17 (* val ((m,_,pt,(p,p_),c)::ss) = [(m,EmptyMout,pt,p,[])];
10.18 - val t = (term_of o the o (parse Isac.thy)) "Rewrite rmult_1 False";
10.19 + val t = (term_of o the o (parse (theory "Isac"))) "Rewrite rmult_1 False";
10.20
10.21 val (ap,(p,p_),c,ss) = (Aundef,p,[],[]);
10.22 assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t;
10.23 @@ -1991,8 +1991,8 @@
10.24 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
10.25 (*
10.26 > val Script sc = (#scr o get_met) ("SqRoot.thy","sqrt-equ-test");
10.27 -> val env = [((term_of o the o (parse Isac.thy)) "bdv",
10.28 - (term_of o the o (parse Isac.thy)) "x")];
10.29 +> val env = [((term_of o the o (parse (theory "Isac"))) "bdv",
10.30 + (term_of o the o (parse (theory "Isac"))) "x")];
10.31 > map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc);
10.32 *)
10.33
11.1 --- a/src/Tools/isac/Interpret/solve.sml Wed Oct 06 14:52:12 2010 +0200
11.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed Oct 06 15:12:41 2010 +0200
11.3 @@ -173,7 +173,7 @@
11.4 ("ok", (map step2taci ss, c', (pt',p')))
11.5 | NotLocatable =>
11.6 let val (p,ps,f,pt) =
11.7 - generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt;
11.8 + generate_hard (assoc_thy "Isac") m (p,Frm) pt;
11.9 in ("not-found-in-script",
11.10 ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
11.11 (*just-before------------------------------------------------------
11.12 @@ -307,7 +307,7 @@
11.13 map step2taci ss, c', (pt',p'))) end
11.14 | NotLocatable =>
11.15 let val (p,ps,f,pt) =
11.16 - generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;
11.17 + generate_hard (assoc_thy "Isac") m (p,p_) pt;
11.18 in ("not-found-in-script",
11.19 ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
11.20 [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
11.21 @@ -424,7 +424,7 @@
11.22 | _ => pos (*somewhere in script*)
11.23 (*val _= tracing"### nxt_solv4 Apply_Method: stored is =";
11.24 val _= tracing(istate2str is);*)
11.25 - val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt;
11.26 + val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
11.27 in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
11.28
11.29
11.30 @@ -564,7 +564,7 @@
11.31 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
11.32 SOME t, is)
11.33 val pos' = ((lev_on o lev_dn) p, Frm)
11.34 - val thy = assoc_thy "Isac.thy"
11.35 + val thy = assoc_thy "Isac"
11.36 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
11.37 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
11.38 val newnds = children (get_nd pt'' p)
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Oct 06 14:52:12 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Oct 06 15:12:41 2010 +0200
12.3 @@ -1,7 +1,7 @@
12.4 (* theory collecting all knowledge
12.5 (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
12.6 for PolynomialEquations.
12.7 - alternative dependencies see Isac.thy
12.8 + alternative dependencies see (theory "Isac")
12.9 created by: rlang
12.10 date: 02.07
12.11 changed by: rlang
13.1 --- a/src/Tools/isac/ProgLang/calculate.sml Wed Oct 06 14:52:12 2010 +0200
13.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Wed Oct 06 15:12:41 2010 +0200
13.3 @@ -215,7 +215,7 @@
13.4 *)
13.5
13.6 (* val ((op_, eval_fn),ct)=(cc,pre);
13.7 - (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;
13.8 + (get_calculation_ (theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
13.9 parse thy ""
13.10 *)
13.11 (*.get a thm from an op_ somewhere in the term;
14.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Wed Oct 06 14:52:12 2010 +0200
14.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Wed Oct 06 15:12:41 2010 +0200
14.3 @@ -418,13 +418,13 @@
14.4 ) handle _ =>
14.5 error ("assoc_thm': '"^thmid^"' not in '"^
14.6 (theory2domID thy)^"' (and parents)");
14.7 -(*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
14.8 +(*> assoc_thm' (theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
14.9 val it = "6 = 2 * 3" : thm
14.10
14.11 -> assoc_thm' Isac.thy ("add_0_left","");
14.12 +> assoc_thm' (theory "Isac") ("add_0_left","");
14.13 val it = "0 + ?z = ?z" : thm
14.14
14.15 -> assoc_thm' Isac.thy ("sym_real_add_zero_left","");
14.16 +> assoc_thm' (theory "Isac") ("sym_real_add_zero_left","");
14.17 val it = "?t = 0 + ?t" [.] : thm
14.18
14.19 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
14.20 @@ -629,7 +629,7 @@
14.21 fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
14.22
14.23 | eval_true' (thy':theory') (rls':rls') (t:term) =
14.24 -(* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres';
14.25 +(* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
14.26 *)
14.27 let val ct' = term2str t;
14.28 in case rewrite_set thy' false rls' ct' of
14.29 @@ -653,7 +653,7 @@
14.30
14.31
14.32
14.33 - rewrite_set_ Isac.thy eval_rls false test_rls
14.34 + rewrite_set_ (theory "Isac") eval_rls false test_rls
14.35 ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
14.36 val xxx = (term_of o the o (parse thy))
14.37 "matches (?a = ?b) (x = #0)";
14.38 @@ -663,7 +663,7 @@
14.39
14.40
14.41
14.42 - rewrite_set_ Isac.thy eval_rls false eval_rls
14.43 + rewrite_set_ (theory "Isac") eval_rls false eval_rls
14.44 ((the o (parse thy)) "contains_root (sqrt #0)");
14.45 val it = SOME ("True",[]) : (cterm * cterm list) option
14.46
15.1 --- a/src/Tools/isac/calcelems.sml Wed Oct 06 14:52:12 2010 +0200
15.2 +++ b/src/Tools/isac/calcelems.sml Wed Oct 06 15:12:41 2010 +0200
15.3 @@ -241,7 +241,7 @@
15.4 val theory2theory' = string_of_thy;
15.5 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
15.6 val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;
15.7 -(*> theory2str' Isac.thy;
15.8 +(*> theory2str' (theory "Isac");
15.9 al it = "Isac" : string
15.10 *)
15.11
15.12 @@ -252,9 +252,9 @@
15.13 else thyID ^ ".thy"
15.14 end;
15.15 (* thyID2theory' "Isac" (*ok*);
15.16 -val it = "Isac.thy" : theory'
15.17 - > thyID2theory' "Isac.thy" (*abuse, goes ok...*);
15.18 -val it = "Isac.thy" : theory'
15.19 +val it = "Isac" : theory'
15.20 + > thyID2theory' "Isac" (*abuse, goes ok...*);
15.21 +val it = "Isac" : theory'
15.22 *)
15.23
15.24 fun theory'2thyID (theory':theory') =
15.25 @@ -263,7 +263,7 @@
15.26 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
15.27 else theory' (*disarm abuse of theory'*)
15.28 end;
15.29 -(* theory'2thyID "Isac.thy";
15.30 +(* theory'2thyID "Isac";
15.31 val it = "Isac" : thyID
15.32 > theory'2thyID "Isac";
15.33 val it = "Isac" : thyID*)
16.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Wed Oct 06 14:52:12 2010 +0200
16.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Wed Oct 06 15:12:41 2010 +0200
16.3 @@ -372,7 +372,7 @@
16.4 fun subs2xml j (subs:subs) =
16.5 (indt j ^"<SUBSTITUTION>\n"^
16.6 foldl op^ ("", map (sub2xml (j+i))
16.7 - (subs2subst (assoc_thy "Isac.thy") subs)) ^
16.8 + (subs2subst (assoc_thy "Isac") subs)) ^
16.9 indt j ^"</SUBSTITUTION>\n"):xml;
16.10 (* val subs = [(str2term "bdv", str2term "x")];
16.11 val subs = ["(bdv, x)"];
16.12 @@ -413,7 +413,7 @@
16.13 if term = e_term
16.14 then indt j ^"<SCRIPT> </SCRIPT>\n"
16.15 else indt j ^"<SCRIPT>\n"^
16.16 - term2xml j (inst_abs (assoc_thy "Isac.thy") term) ^ "\n" ^
16.17 + term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
16.18 indt j ^"</SCRIPT>\n"
16.19 | scr2xml j (Rfuns _) =
16.20 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
17.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed Oct 06 14:52:12 2010 +0200
17.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed Oct 06 15:12:41 2010 +0200
17.3 @@ -108,7 +108,7 @@
17.4 str2term ("Problem (" ^
17.5 (get_thy o theory2domID) thy ^ "_, " ^
17.6 (strs2str' o rev) pblRD ^ ")");
17.7 -(* term2str (pbl2term Isac.thy ["equations","univariate","normalize"]);
17.8 +(* term2str (pbl2term (theory "Isac") ["equations","univariate","normalize"]);
17.9 val it = "Problem (Isac, [normalize, univariate, equations])" : string
17.10 *)
17.11
17.12 @@ -213,7 +213,7 @@
17.13 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
17.14 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
17.15 crls,erls,nrls,prls,srls,rew_ord'}:met) =
17.16 - let val thy' = "Isac.thy" (*FIXME.WN0607 get thy from met ?!?*)
17.17 + let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
17.18 val crls' = (#id o rep_rls) crls
17.19 val erls' = (#id o rep_rls) erls
17.20 val nrls' = (#id o rep_rls) nrls
18.1 --- a/test/Tools/isac/Frontend/interface.sml Wed Oct 06 14:52:12 2010 +0200
18.2 +++ b/test/Tools/isac/Frontend/interface.sml Wed Oct 06 15:12:41 2010 +0200
18.3 @@ -701,7 +701,7 @@
18.4 DEconstrCalcTree 1;
18.5 CalcTree
18.6 [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],
18.7 - ("Isac.thy",
18.8 + ("Isac",
18.9 ["univariate","equation"],
18.10 ["no_met"]))];
18.11 Iterator 1;
19.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Oct 06 14:52:12 2010 +0200
19.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Oct 06 15:12:41 2010 +0200
19.3 @@ -101,13 +101,13 @@
19.4
19.5 *)
19.6 "----------------------------------------------------------";
19.7 - val fod = make_deriv Isac.thy Atools_erls
19.8 + val fod = make_deriv (theory "Isac") Atools_erls
19.9 ((#rules o rep_rls) Test_simplify)
19.10 (sqrt_right false (theory "Pure")) NONE
19.11 (str2term "x + 1 + -1 * 2 = 0");
19.12 (writeln o trtas2str) fod;
19.13
19.14 - val ifod = make_deriv Isac.thy Atools_erls
19.15 + val ifod = make_deriv (theory "Isac") Atools_erls
19.16 ((#rules o rep_rls) Test_simplify)
19.17 (sqrt_right false (theory "Pure")) NONE
19.18 (str2term "-2 * 1 + (1 + x) = 0");
19.19 @@ -544,7 +544,7 @@
19.20 [], NONE,
19.21 ??.empty, Sundef, false)*)
19.22 print_depth 5; spec; print_depth 3;
19.23 -(*("Isac.thy",
19.24 +(*("Isac",
19.25 ["derivative_of", "function"],
19.26 ["diff", "differentiate_on_R"]) : spec*)
19.27 writeln (itms2str_ ctxt probl);
19.28 @@ -574,7 +574,7 @@
19.29 (*the following input is copied from BridgeLog Java <==> SML,
19.30 omitting unnecessary inputs*)
19.31 (*1>*)states:=[];
19.32 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac.thy",["derivative_of","function"],["diff","differentiate_on_R"]))];
19.33 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
19.34 (*3>*)Iterator 1; moveActiveRoot 1;
19.35
19.36 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
19.37 @@ -589,7 +589,7 @@
19.38 [], NONE,
19.39 ??.empty, Sundef, false)*)
19.40 print_depth 5; spec; print_depth 3;
19.41 -(*("Isac.thy",
19.42 +(*("Isac",
19.43 ["derivative_of", "function"],
19.44 ["diff", "differentiate_on_R"]) : spec*)
19.45 writeln (itms2str_ ctxt probl);
20.1 --- a/test/Tools/isac/Interpret/ptyps.sml Wed Oct 06 14:52:12 2010 +0200
20.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Wed Oct 06 15:12:41 2010 +0200
20.3 @@ -71,7 +71,7 @@
20.4 show_ptyps();
20.5
20.6 (*case 1: no refinement *)
20.7 -val thy = Isac.thy;
20.8 +val thy = (theory "Isac");
20.9 val (d1,ts1) = split_dts thy ((term_of o the o (parse thy))
20.10 "fixedValues [aaa=0]");
20.11 val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
21.1 --- a/test/Tools/isac/Interpret/rewtools.sml Wed Oct 06 14:52:12 2010 +0200
21.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Oct 06 15:12:41 2010 +0200
21.3 @@ -442,7 +442,7 @@
21.4 "----- these work ?!?";
21.5 val th = sym_thm real_minus_eq_cancel;
21.6 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
21.7 -val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
21.8 +val th'= mk_thm (theory "Isac") ((de_quote o string_of_thm) real_minus_eq_cancel);
21.9 val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
21.10
21.11 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
21.12 @@ -504,7 +504,7 @@
21.13 "----------- fun filter_appl_rews --------------------------------";
21.14 "----------- fun filter_appl_rews --------------------------------";
21.15 val f = str2term "a + z + 2*a + 3*z + 5 + 6";
21.16 -val thy = assoc_thy "Isac.thy";
21.17 +val thy = assoc_thy "Isac";
21.18 val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
21.19 val rls = Test_simplify;
21.20 (* val rls = rls_p_33; filter_appl_rews ---> length 2
22.1 --- a/test/Tools/isac/Knowledge/algein.sml Wed Oct 06 14:52:12 2010 +0200
22.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Oct 06 15:12:41 2010 +0200
22.3 @@ -128,7 +128,7 @@
22.4 "----------- Widerspruch 3 = 777 ---------------------------------";
22.5 "----------- Widerspruch 3 = 777 ---------------------------------";
22.6 "----------- Widerspruch 3 = 777 ---------------------------------";
22.7 -val thy = Isac.thy;
22.8 +val thy = (theory "Isac");
22.9 val rew_ord = dummy_ord;
22.10 val erls = Erls;
22.11
23.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Wed Oct 06 14:52:12 2010 +0200
23.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Oct 06 15:12:41 2010 +0200
23.3 @@ -722,7 +722,7 @@
23.4 "--- script expression 1";
23.5 val screxp1_ = str2term "Take (nth_ 1 (rb_::bool list))";
23.6 val screxp1 = subst_atomic [(rb_, rb)] screxp1_; term2str screxp1;
23.7 -val SOME (b1,_) = rewrite_set_ Isac.thy false srls2 screxp1; term2str b1;
23.8 +val SOME (b1,_) = rewrite_set_ (theory "Isac") false srls2 screxp1; term2str b1;
23.9 if term2str b1 = "Take (y 0 = 0)" then ()
23.10 else error "biegelinie.sml: rew. Bieglie2 --1";
23.11 val b1 = str2term "(y 0 = 0)";
23.12 @@ -731,7 +731,7 @@
23.13 val screxp2_ = str2term "filter (sameFunId (lhs b1_)) funs_";
23.14 val b1_ = str2term "b1_::bool";
23.15 val screxp2 = subst_atomic [(b1_,b1),(funs_,funs)] screxp2_; term2str screxp2;
23.16 -val SOME (fs,_) = rewrite_set_ Isac.thy false srls2 screxp2; term2str fs;
23.17 +val SOME (fs,_) = rewrite_set_ (theory "Isac") false srls2 screxp2; term2str fs;
23.18 if term2str fs = "[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 ()
23.19 else error "biegelinie.sml: rew. Bieglie2 --2";
23.20
23.21 @@ -742,7 +742,7 @@
23.22 val fs_ = str2term "fs_::bool list";
23.23 val screxp3 = subst_atomic [(fs_,fs),(b1_,b1)] screxp3_;
23.24 writeln (term2str screxp3);
23.25 -val SOME (equ,_) = rewrite_set_ Isac.thy false srls2 screxp3;
23.26 +val SOME (equ,_) = rewrite_set_ (theory "Isac") false srls2 screxp3;
23.27 if term2str equ = "SubProblem\n (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])\n [BOOL\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)),\n BOOL (y 0 = 0)]" then ()
23.28 else error "biegelinie.sml: rew. Bieglie2 --3";
23.29 writeln (term2str equ);
24.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Oct 06 14:52:12 2010 +0200
24.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Oct 06 15:12:41 2010 +0200
24.3 @@ -104,7 +104,7 @@
24.4 val ct = "d_d s a";
24.5 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
24.6 (*got: NONE instead SOME*)
24.7 -eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls");
24.8 +eval_true (theory "Isac") [str2term "a is_const"] (assoc_rls"erls");
24.9 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*)
24.10 val SOME (ctt,_) =
24.11 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
24.12 @@ -263,11 +263,11 @@
24.13 trace_rewrite:=true;
24.14 val t = str2term ct;
24.15 term2str t;
24.16 - val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
24.17 + val SOME (t',_) = rewrite_set_ (theory "Isac") false make_polynomial t;
24.18 term2str t';
24.19 trace_rewrite:=false;
24.20
24.21 - val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';
24.22 + val SOME (t'',_) = rewrite_set_ (theory "Isac") false make_polynomial t';
24.23 term2str t'';
24.24
24.25 val thm = num_str @{thm realpow_eq_oneI;
24.26 @@ -481,7 +481,7 @@
24.27 term2str screxp1;
24.28 atomty screxp1;
24.29
24.30 -val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1;
24.31 +val SOME (f'_,_) = rewrite_set_ (theory "Isac") false srls_diff screxp1;
24.32 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
24.33 else error "diff.sml: diff.behav. in 'primed'";
24.34 atomty f'_;
24.35 @@ -666,7 +666,7 @@
24.36 val f = str2term "G' = d_d l (l * sqrt (7 * s ^ 2 - l ^ 2))";
24.37 (*
24.38 trace_rewrite := true;
24.39 -rewrite_inst_ Isac.thy tless_true erls_diff true subs diff_prod_const f;
24.40 +rewrite_inst_ (theory "Isac") tless_true erls_diff true subs diff_prod_const f;
24.41 trace_rewrite := false;
24.42 *)
24.43
25.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Oct 06 14:52:12 2010 +0200
25.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Oct 06 15:12:41 2010 +0200
25.3 @@ -179,7 +179,7 @@
25.4 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
25.5 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
25.6 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
25.7 -val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
25.8 +val thy = (theory "Isac") (*because of Undeclared constant "Biegelinie.EI*);
25.9 val t =
25.10 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
25.11 \ -1 * q_0 / 24 * 0 ^^^ 4),\
26.1 --- a/test/Tools/isac/Knowledge/equation.sml Wed Oct 06 14:52:12 2010 +0200
26.2 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Oct 06 15:12:41 2010 +0200
26.3 @@ -6,7 +6,7 @@
26.4 use"../smltest/IsacKnowledge/equation.sml";
26.5 use"equation.sml";
26.6 *)
26.7 -val thy = Isac.thy;
26.8 +val thy = (theory "Isac");
26.9
26.10 "-----------------------------------------------------------------";
26.11 "table of contents -----------------------------------------------";
27.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Oct 06 14:52:12 2010 +0200
27.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Oct 06 15:12:41 2010 +0200
27.3 @@ -402,8 +402,9 @@
27.4 ("Integrate",["integrate","function"],
27.5 ["diff","integration"]);
27.6 val p = e_pos'; val c = [];
27.7 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
27.8 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.9 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Pr*)
27.10 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...)*)
27.11 +(*=== inhibit exn ?=============================================================
27.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.15 @@ -417,7 +418,6 @@
27.16 else error "integrate.sml: method [diff,integration]";
27.17
27.18
27.19 -(*=== inhibit exn ?=============================================================
27.20 "----------- me method [diff,integration,named] ---------";
27.21 "----------- me method [diff,integration,named] ---------";
27.22 "----------- me method [diff,integration,named] ---------";
28.1 --- a/test/Tools/isac/Knowledge/logexp.sml Wed Oct 06 14:52:12 2010 +0200
28.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed Oct 06 15:12:41 2010 +0200
28.3 @@ -23,7 +23,7 @@
28.4
28.5 equality_power;
28.6 exp_invers_log;
28.7 -(* WN071203 ???... wrong thy ?!? because parsing with Isac.thy works ?
28.8 +(* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac") works ?
28.9 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
28.10 ["equation","test"];
28.11 *)
29.1 --- a/test/Tools/isac/Knowledge/poly.sml Wed Oct 06 14:52:12 2010 +0200
29.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Oct 06 15:12:41 2010 +0200
29.3 @@ -551,7 +551,7 @@
29.4
29.5 (*WN071202: ^^^ why then is there no rewriting ...*)
29.6 val term = str2term "2*b + (3*a + 3*b)";
29.7 -val NONE = rewrite_set_ Isac.thy false order_add_mult term;
29.8 +val NONE = rewrite_set_ (theory "Isac") false order_add_mult term;
29.9
29.10 (*or why is there no rewriting this way...*)
29.11 val t1 = str2term "2 * b + (3 * a + 3 * b)";
30.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Oct 06 14:52:12 2010 +0200
30.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Oct 06 15:12:41 2010 +0200
30.3 @@ -409,16 +409,16 @@
30.4 val erls = erls_ordne_alphabetisch;
30.5 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
30.6 val SOME (t',_) =
30.7 - rewrite_ Isac.thy e_rew_ord erls false tausche_minus t;
30.8 + rewrite_ (theory "Isac") e_rew_ord erls false tausche_minus t;
30.9 term2str t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
30.10
30.11 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
30.12 val NONE =
30.13 - rewrite_ Isac.thy e_rew_ord erls false tausche_minus_plus t;
30.14 + rewrite_ (theory "Isac") e_rew_ord erls false tausche_minus_plus t;
30.15
30.16 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
30.17 val SOME (t',_) =
30.18 - rewrite_set_ Isac.thy false ordne_alphabetisch t;
30.19 + rewrite_set_ (theory "Isac") false ordne_alphabetisch t;
30.20 term2str t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
30.21 trace_rewrite := false;
30.22
31.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Wed Oct 06 14:52:12 2010 +0200
31.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Oct 06 15:12:41 2010 +0200
31.3 @@ -2,7 +2,7 @@
31.4 use"rootrateq.sml";
31.5 *)
31.6
31.7 -val thy = Isac.thy;
31.8 +val thy = (theory "Isac");
31.9
31.10 "--------------------- tests on predicates -------------------------------";
31.11 "--------------------- tests on predicates -------------------------------";
32.1 --- a/test/Tools/isac/Knowledge/termorder.sml Wed Oct 06 14:52:12 2010 +0200
32.2 +++ b/test/Tools/isac/Knowledge/termorder.sml Wed Oct 06 15:12:41 2010 +0200
32.3 @@ -173,7 +173,7 @@
32.4 use_thy"Isac";
32.5
32.6 get_thm Termorder.thy "bdv_n_collect";
32.7 - get_thm Isac.thy "bdv_n_collect";
32.8 + get_thm (theory "Isac") "bdv_n_collect";
32.9
32.10 *)
32.11 val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
33.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Oct 06 14:52:12 2010 +0200
33.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Oct 06 15:12:41 2010 +0200
33.3 @@ -103,7 +103,7 @@
33.4 "bound_variable x","error_bound 0"(*,
33.5 "solutions L::real set" ,
33.6 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
33.7 -val thy = Isac.thy;
33.8 +val thy = (theory "Isac");
33.9 val formals = map (the o (parse thy)) origin;
33.10
33.11 val given = ["equation (l=(r::real))",
34.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Wed Oct 06 14:52:12 2010 +0200
34.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Wed Oct 06 15:12:41 2010 +0200
34.3 @@ -8,7 +8,7 @@
34.4
34.5 (*---------------- 25.7.02 ---------------------*)
34.6
34.7 -val thy = Isac.thy;
34.8 +val thy = (theory "Isac");
34.9 val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
34.10 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;
34.11
34.12 @@ -37,25 +37,25 @@
34.13 val t = (term_of o the o (parse Test.thy))
34.14 "is_rootequation_in (sqrt(x)=1) x";
34.15 atomty t;
34.16 -val t = (term_of o the o (parse Isac.thy))
34.17 +val t = (term_of o the o (parse (theory "Isac")))
34.18 "is_rootequation_in (sqrt(x)=1) x";
34.19 atomty t;
34.20
34.21 (*
34.22 val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;
34.23 *)
34.24 -val SOME(tt,_) = rewrite_set_ Isac.thy true tval_rls t;
34.25 +val SOME(tt,_) = rewrite_set_ (theory "Isac") true tval_rls t;
34.26
34.27 -rewrite_set "Isac.thy" true
34.28 +rewrite_set "Isac" true
34.29 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
34.30 rewrite_set "Test.thy" true
34.31 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
34.32
34.33
34.34 -(*WN: ^^^--- bitte nimm vorerst immer Isac.thy, damit wird richtig gematcht,
34.35 +(*WN: ^^^--- bitte nimm vorerst immer (theory "Isac"), damit wird richtig gematcht,
34.36 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
34.37 store_pbt
34.38 - (prep_pbt (*Test.thy*) Isac.thy
34.39 + (prep_pbt (*Test.thy*) (theory "Isac")
34.40 (["root'","univariate","equation","test"],
34.41 [("#Given" ,["equality e_e","solveFor v_v"]),
34.42 ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
34.43 @@ -71,7 +71,7 @@
34.44 (*---------------- 29.7.02 ---------------------*)
34.45
34.46 store_pbt
34.47 - (prep_pbt Isac.thy
34.48 + (prep_pbt (theory "Isac")
34.49 (["approximate","univariate","equation","test"],
34.50 [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),
34.51 ("#Where" ,["matches (?a = ?b) e_e"]),
34.52 @@ -83,7 +83,7 @@
34.53 methods:= overwritel (!methods,
34.54 [
34.55 prep_met
34.56 - (("Isac.thy","solve_univar_err"):metID,
34.57 + (("Isac","solve_univar_err"):metID,
34.58 [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),
34.59 ("#Find" ,["solutions v_i_"])
34.60 ],
34.61 @@ -100,8 +100,8 @@
34.62 val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",
34.63 "solutions L"];
34.64 val (dI',pI',mI') =
34.65 - ("Isac.thy",["approximate","univariate","equation","test"],
34.66 - ("Isac.thy","solve_univar_err"));
34.67 + ("Isac",["approximate","univariate","equation","test"],
34.68 + ("Isac","solve_univar_err"));
34.69 val p = e_pos'; val c = [];
34.70 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
34.71 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
34.72 @@ -112,7 +112,7 @@
34.73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.76 -(*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)
34.77 +(*val nxt = ("Apply_Method",Apply_Method ("Isac","solve_univar_err"))*)
34.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.79 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
34.80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.81 @@ -139,8 +139,8 @@
34.82 val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",
34.83 "solutions L"];
34.84 val (dI',pI',mI') =
34.85 - ("Isac.thy",["approximate","univariate","equation","test"],
34.86 - ("Isac.thy","solve_univar_err"));
34.87 + ("Isac",["approximate","univariate","equation","test"],
34.88 + ("Isac","solve_univar_err"));
34.89 val p = e_pos'; val c = [];
34.90 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
34.91 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
34.92 @@ -151,7 +151,7 @@
34.93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.96 -(*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)
34.97 +(*val nxt = ("Apply_Method",Apply_Method ("Isac","solve_univar_err"))*)
34.98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34.99 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
34.100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
35.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Oct 06 14:52:12 2010 +0200
35.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Oct 06 15:12:41 2010 +0200
35.3 @@ -190,7 +190,7 @@
35.4 (*val it = SOME (Const ("True","bool"),[]) ... works*)
35.5
35.6 val t = str2term "2 * x is_const";
35.7 - val SOME (str,t') = eval_const "" "" t Isac.thy;
35.8 + val SOME (str,t') = eval_const "" "" t (theory "Isac");
35.9 term2str t';
35.10
35.11
35.12 @@ -315,7 +315,7 @@
35.13 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
35.14 " ================= calculate.sml:10.8.02 2002:///->/ ======== ";
35.15 " ----------------- rewriting works ? -----------------------";
35.16 - val thy = Isac.thy;
35.17 + val thy = (theory "Isac");
35.18 val prop = (#prop o rep_thm) real_divide_1;
35.19 atomty prop;
35.20 (*** -------------
36.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed Oct 06 14:52:12 2010 +0200
36.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed Oct 06 15:12:41 2010 +0200
36.3 @@ -8,7 +8,7 @@
36.4 CAUTION with testing *2file functions -- they are actually writing !!!
36.5 *)
36.6
36.7 -val thy = Isac.thy;
36.8 +val thy = (theory "Isac");
36.9
36.10 "-----------------------------------------------------------------";
36.11 "table of contents -----------------------------------------------";
37.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Oct 06 14:52:12 2010 +0200
37.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Oct 06 15:12:41 2010 +0200
37.3 @@ -8,7 +8,7 @@
37.4 CAUTION with testing *2file functions -- they are actually writing to ~/tmp
37.5 *)
37.6
37.7 -val thy = Isac.thy;
37.8 +val thy = (theory "Isac");
37.9
37.10 "-----------------------------------------------------------------";
37.11 "table of contents -----------------------------------------------";