1.1 --- a/src/Tools/isac/Build_Test_Isac.thy Mon Oct 11 12:55:40 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Test_Isac.thy Mon Oct 11 13:31:22 2010 +0200
1.3 @@ -21,8 +21,9 @@
1.4
1.5 use_thy "Build_Isac"
1.6
1.7 -(* PROCEEDING WITH TESTS HERE DOESN'T WORK,
1.8 - because the 'imports "Knowledge/Isac" is required; for instance:
1.9 +(* PROCEEDING WITH 'use testfile.sml" HERE DOESN'T WORK,
1.10 + because the 'imports "Knowledge/Isac" (in Test_Isac.thy) is required;
1.11 + the following kind of errors are raised:
1.12 use "../../../test/Tools/isac/Interpret/calchead.sml"
1.13 *** get_pbt not found: ["linear","system"]
1.14 use"../../../test/Tools/isac/Knowledge/integrate.sml";
2.1 --- a/src/Tools/isac/Frontend/interface.sml Mon Oct 11 12:55:40 2010 +0200
2.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Oct 11 13:31:22 2010 +0200
2.3 @@ -120,10 +120,10 @@
2.4 but remember the envisaged changes for fun autoCalculate;
2.5 compare force NextTactic .*)
2.6 (* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
2.7 - val (cI, tac) = (1, Specify_Theory "PolyEq.thy");
2.8 + val (cI, tac) = (1, Specify_Theory "PolyEq");
2.9 val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
2.10 "univariate","equation"]);
2.11 - val (cI, tac) = (1, Subproblem ("Poly.thy",
2.12 + val (cI, tac) = (1, Subproblem ("Poly",
2.13 ["polynomial","univariate","equation"]));
2.14 val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]);
2.15 val (cI, tac) = (1, Detail_Set "Test_simplify");
2.16 @@ -230,14 +230,14 @@
2.17 [Given ["fixedValues [r=Arbfix]"],
2.18 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.19 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
2.20 - ("DiffApp.thy", ["maximum_of","function"],
2.21 + ("DiffApp", ["maximum_of","function"],
2.22 ["DiffApp","max_by_calculus"])));
2.23 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
2.24 (1, (([],Pbl),"solve (x+1=2, x)",
2.25 [Given ["equality (x+1=2)", "solveFor x"],
2.26 Find ["solutions L"]],
2.27 Pbl,
2.28 - ("Test.thy", ["linear","univariate","equation","test"],
2.29 + ("Test", ["linear","univariate","equation","test"],
2.30 ["Test","solve_linear"])));
2.31 val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
2.32 (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Oct 11 12:55:40 2010 +0200
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Oct 11 13:31:22 2010 +0200
3.3 @@ -1766,7 +1766,7 @@
3.4 | nxt_model_pbl tac_ _ =
3.5 error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
3.6 (* run subp_rooteq.sml ''
3.7 - until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
3.8 + until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
3.9 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
3.10 (last_elem o drop_last) ets'';
3.11 > val mst = (last_elem o drop_last) ets'';
4.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Oct 11 12:55:40 2010 +0200
4.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Oct 11 13:31:22 2010 +0200
4.3 @@ -432,7 +432,7 @@
4.4 [Given ["fixedValues [r=Arbfix]"],
4.5 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
4.6 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
4.7 - ("DiffApp.thy", ["e_pblID"], ["e_metID"]));
4.8 + ("DiffApp", ["e_pblID"], ["e_metID"]));
4.9 val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd;
4.10 *)
4.11 fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
5.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Oct 11 12:55:40 2010 +0200
5.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Oct 11 13:31:22 2010 +0200
5.3 @@ -403,13 +403,13 @@
5.4
5.5 (*.which theory below thy' contains a theorem; this can be in isabelle !
5.6 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
5.7 -(* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy));
5.8 - val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
5.9 +(* val (str, (_, thy)) = ("real_diff_minus", ("Root", Root.thy));
5.10 + val (str, (_, thy)) = ("real_diff_minus", ("Poly", Poly.thy));
5.11 *)
5.12 fun thy_contains_thm (str:xstring) (_, thy) =
5.13 member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str;
5.14 (* val (thy', str) = ("Isac", "real_mult_minus1");
5.15 - val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
5.16 + val (thy', str) = ("PolyMinus", "klammer_minus_plus");
5.17 *)
5.18 fun thy_containing_thm (thy':theory') (str:xstring) =
5.19 let val thy' = thyID2theory' thy'
5.20 @@ -429,7 +429,7 @@
5.21
5.22 (*.which theory below thy' contains a ruleset;
5.23 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
5.24 -(* val (thy', rls') = ("PolyEq.thy", "separate_bdv");
5.25 +(* val (thy', rls') = ("PolyEq", "separate_bdv");
5.26 *)
5.27 local infix mem; (*from Isabelle2002*)
5.28 fun x mem [] = false
6.1 --- a/src/Tools/isac/Interpret/script.sml Mon Oct 11 12:55:40 2010 +0200
6.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Oct 11 13:31:22 2010 +0200
6.3 @@ -243,10 +243,10 @@
6.4 ("itr_arg not impl. for " ^
6.5 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt (assoc_thy thy))) t));
6.6 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
6.7 -> itr_arg "Script.thy" t;
6.8 +> itr_arg "Script" t;
6.9 val it = Free ("e_","RealDef.real") : term
6.10 > val t = (term_of o the o (parse thy))"xxx";
6.11 -> itr_arg "Script.thy" t;
6.12 +> itr_arg "Script" t;
6.13 *** itr_arg not impl. for xxx
6.14 uncaught exception ERROR
6.15 raised at: library.ML:1114.35-1114.40*)
6.16 @@ -343,7 +343,7 @@
6.17 in (flat o (map (itm2arg itms))) pats end;
6.18 (*
6.19 > val sc = ... Solve_root_equation ...
6.20 -> val mI = ("Script.thy","sqrt-equ-test");
6.21 +> val mI = ("Script","sqrt-equ-test");
6.22 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
6.23 > val ts = itms2args thy mI itms;
6.24 > map (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) ts;
6.25 @@ -443,7 +443,7 @@
6.26 Free (dI',_) $
6.27 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
6.28 (*compare "| assod _ (Subproblem'"*)
6.29 - let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^".thy"*);
6.30 + let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^""*);
6.31 val thy = maxthy (assoc_thy dI) (rootthy pt);
6.32 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
6.33 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
6.34 @@ -485,7 +485,7 @@
6.35 "(SubProblem (SqRoot_,[equation,univariate],(SqRoot_,solve_linear))\
6.36 \ [BOOL e_, REAL v_])::bool list";
6.37 > stac2tac_ pt SqRoot.thy t;
6.38 -val it = (Subproblem ("SqRoot.thy",[#,#]),Const (#,#) $ (# $ # $ (# $ #)))
6.39 +val it = (Subproblem ("SqRoot",[#,#]),Const (#,#) $ (# $ # $ (# $ #)))
6.40 *)
6.41
6.42 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
6.43 @@ -557,7 +557,7 @@
6.44
6.45 (*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
6.46 > val f'= (term_of o the o (parse thy))"#0+(sqrt(sqrt a))^^^#2=#0";
6.47 -> val m = Rewrite'("Script.thy","tless_true","eval_rls",false,
6.48 +> val m = Rewrite'("Script","tless_true","eval_rls",false,
6.49 ("rroot_square_inv",""),f,(f',[]));
6.50 > val stac = (term_of o the o (parse thy))
6.51 "Rewrite rroot_square_inv False (#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0)";
6.52 @@ -654,7 +654,7 @@
6.53 Free (dI',_) $
6.54 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
6.55 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
6.56 - let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^".thy"*);
6.57 + let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^""*);
6.58 val thy = maxthy (assoc_thy dI) (rootthy pt);
6.59 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
6.60 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
6.61 @@ -813,7 +813,7 @@
6.62 > lhs = tt;
6.63 val it = true : bool
6.64 > rep_tac_ (Rewrite_Inst'
6.65 - ("Script.thy","tless_true","eval_rls",false,subs,
6.66 + ("Script","tless_true","eval_rls",false,subs,
6.67 ("square_equation_left",""),f,(f',[])));
6.68 *)
6.69 | rep_tac_ (Rewrite' (thy',rod,rls,put,(thmID,thm),f,(f',asm)))=
6.70 @@ -831,7 +831,7 @@
6.71 > val f' = (term_of o the o (parse thy)) "x=#3";
6.72 > val Thm (id,thm) =
6.73 rep_tac_ (Rewrite'
6.74 - ("Script.thy","tless_true","eval_rls",false,
6.75 + ("Script","tless_true","eval_rls",false,
6.76 ("square_equation_left",""),f,(f',[])));
6.77 > val SOME ct = parse thy
6.78 "Rewrite square_equation_left True (x=#1+#2)";
6.79 @@ -854,7 +854,7 @@
6.80 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
6.81 (* ... vals from Rewrite_Inst' ...
6.82 > rep_tac_ (Rewrite_Set_Inst'
6.83 - ("Script.thy",false,subs,
6.84 + ("Script",false,subs,
6.85 "isolate_bdv",f,(f',[])));
6.86 *)
6.87 (* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
6.88 @@ -878,7 +878,7 @@
6.89 > val f' = (term_of o the o (parse thy)) "x=#3";
6.90 > val Thm (id,thm) =
6.91 rep_tac_ (Rewrite_Set'
6.92 - ("Script.thy",false,"SqRoot_simplify",f,(f',[])));
6.93 + ("Script",false,"SqRoot_simplify",f,(f',[])));
6.94 val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
6.95 val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
6.96 *)
6.97 @@ -1927,7 +1927,7 @@
6.98 in map ((stac2tac pt thy) o rep_stacexpr o #2 o
6.99 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
6.100 (*
6.101 -> val Script sc = (#scr o get_met) ("SqRoot.thy","sqrt-equ-test");
6.102 +> val Script sc = (#scr o get_met) ("SqRoot","sqrt-equ-test");
6.103 > val env = [((term_of o the o (parse (theory "Isac"))) "bdv",
6.104 (term_of o the o (parse (theory "Isac"))) "x")];
6.105 > map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc);
7.1 --- a/src/Tools/isac/Knowledge/Isac.thy Mon Oct 11 12:55:40 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Mon Oct 11 13:31:22 2010 +0200
7.3 @@ -43,12 +43,12 @@
7.4 including thms from Isabelle used in rls;
7.5 elements store_*d in any *.thy are not overwritten.*)
7.6
7.7 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
7.8 thehier := the_hier (!thehier) (collect_thydata ());
7.9 tracing("----------------------------------\n" ^
7.10 "*** insert: not found ... IS OK : \n" ^
7.11 "comes from fill_parents \n" ^
7.12 "----------------------------------\n");
7.13 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
7.14 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
7.15 *}
7.16
8.1 --- a/src/Tools/isac/ProgLang/Script.thy Mon Oct 11 12:55:40 2010 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Script.thy Mon Oct 11 13:31:22 2010 +0200
8.3 @@ -144,7 +144,7 @@
8.4 "letpar x = a in e" == "Letpar a (%x. e)"
8.5 *** Error in syntax translation rule: rhs contains extra variables
8.6 *** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
8.7 -*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy").
8.8 +*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script").
8.9 *)
8.10
8.11 ML {* (*the former Script.ML*)
9.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Oct 11 12:55:40 2010 +0200
9.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Oct 11 13:31:22 2010 +0200
9.3 @@ -445,7 +445,7 @@
9.4 end;
9.5
9.6 (*
9.7 -val thy = "RatArith.thy";
9.8 +val thy = "RatArith";
9.9 val rew_ord = "dummy_ord";
9.10 > val rls = "eval_rls";
9.11 val put_asm = true;
9.12 @@ -480,7 +480,7 @@
9.13 should work on term, and stand in Isa99/rewrite-parse.sml,
9.14 but there list_rls <- eval_binop is not yet defined*)
9.15 (*fun eval_listexpr' ct =
9.16 - let val rew = rewrite_set "ListC.thy" false "list_rls" ct;
9.17 + let val rew = rewrite_set "ListC" false "list_rls" ct;
9.18 in case rew of
9.19 SOME (res,_) => res
9.20 | NONE => ct end;-----------------30.9.02---*)
9.21 @@ -547,7 +547,7 @@
9.22 ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
9.23 ((snd o split_list) subs);
9.24
9.25 -> val thy' = "RatArith.thy";
9.26 +> val thy' = "RatArith";
9.27 > val subs = [("bdv","x::rat"),("zzz","z::nat")];
9.28 > (the o (parse (assoc_thy thy'))) "x::rat";
9.29 > (#T o rep_cterm o the o (parse (assoc_thy thy')));
10.1 --- a/src/Tools/isac/calcelems.sml Mon Oct 11 12:55:40 2010 +0200
10.2 +++ b/src/Tools/isac/calcelems.sml Mon Oct 11 13:31:22 2010 +0200
10.3 @@ -230,8 +230,8 @@
10.4 the latter have a thmid "#..."
10.5 and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
10.6 and have a special assoc_thm / assoc_rls in this interface *)
10.7 -type theory' = string; (* = domID ^".thy" *)
10.8 -type domID = string; (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
10.9 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
10.10 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
10.11 type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
10.12
10.13 fun string_of_thy thy = Context.theory_name thy: theory';
10.14 @@ -244,24 +244,28 @@
10.15 al it = "Isac" : string
10.16 *)
10.17
10.18 -fun thyID2theory' (thyID:thyID) =
10.19 +fun thyID2theory' (thyID:thyID) = thyID;
10.20 +(*
10.21 let val ss = explode thyID
10.22 val ext = implode (takelast (4, ss))
10.23 in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
10.24 else thyID ^ ".thy"
10.25 end;
10.26 +*)
10.27 (* thyID2theory' "Isac" (*ok*);
10.28 val it = "Isac" : theory'
10.29 > thyID2theory' "Isac" (*abuse, goes ok...*);
10.30 val it = "Isac" : theory'
10.31 *)
10.32
10.33 -fun theory'2thyID (theory':theory') =
10.34 +fun theory'2thyID (theory':theory') = theory';
10.35 +(*
10.36 let val ss = explode theory'
10.37 val ext = implode (takelast (4, ss))
10.38 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
10.39 else theory' (*disarm abuse of theory'*)
10.40 end;
10.41 +*)
10.42 (* theory'2thyID "Isac";
10.43 val it = "Isac" : thyID
10.44 > theory'2thyID "Isac";
11.1 --- a/test/Tools/isac/Frontend/interface.sml Mon Oct 11 12:55:40 2010 +0200
11.2 +++ b/test/Tools/isac/Frontend/interface.sml Mon Oct 11 13:31:22 2010 +0200
11.3 @@ -94,7 +94,7 @@
11.4 states := [];
11.5 CalcTree (*start of calculation, return No.1*)
11.6 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
11.7 - ("Test.thy",
11.8 + ("Test",
11.9 ["linear","univariate","equation","test"],
11.10 ["Test","solve_linear"]))];
11.11 Iterator 1; (*create an active Iterator on CalcTree No.1*)
11.12 @@ -132,7 +132,7 @@
11.13 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.14
11.15 fetchProposedTactic 1;
11.16 - setNextTactic 1 (Specify_Theory "Test.thy");
11.17 + setNextTactic 1 (Specify_Theory "Test");
11.18 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.19 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
11.20
11.21 @@ -215,7 +215,7 @@
11.22 states:=[];
11.23 CalcTree (*start of calculation, return No.1*)
11.24 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.25 - ("Test.thy",
11.26 + ("Test",
11.27 ["sqroot-test","univariate","equation","test"],
11.28 ["Test","squ-equ-test-subpbl1"]))];
11.29 Iterator 1;
11.30 @@ -239,7 +239,7 @@
11.31 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.32
11.33 fetchProposedTactic 1;
11.34 - setNextTactic 1 (Specify_Theory "Test.thy");
11.35 + setNextTactic 1 (Specify_Theory "Test");
11.36 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.37
11.38 fetchProposedTactic 1;
11.39 @@ -265,7 +265,7 @@
11.40 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.41
11.42 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
11.43 - setNextTactic 1 (Subproblem ("Test.thy",
11.44 + setNextTactic 1 (Subproblem ("Test",
11.45 ["linear","univariate","equation","test"]));
11.46 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.47
11.48 @@ -286,7 +286,7 @@
11.49 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.50
11.51 fetchProposedTactic 1;
11.52 - setNextTactic 1 (Specify_Theory "Test.thy");
11.53 + setNextTactic 1 (Specify_Theory "Test");
11.54 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
11.55
11.56 fetchProposedTactic 1;
11.57 @@ -341,7 +341,7 @@
11.58 states:=[];
11.59 CalcTree
11.60 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.61 - ("Test.thy",
11.62 + ("Test",
11.63 ["sqroot-test","univariate","equation","test"],
11.64 ["Test","squ-equ-test-subpbl1"]))];
11.65 Iterator 1;
11.66 @@ -395,7 +395,7 @@
11.67 states:=[];
11.68 CalcTree
11.69 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
11.70 - ("Test.thy",
11.71 + ("Test",
11.72 ["linear","univariate","equation","test"],
11.73 ["Test","solve_linear"]))];
11.74 Iterator 1;
11.75 @@ -419,7 +419,7 @@
11.76 states:=[];
11.77 CalcTree
11.78 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
11.79 - ("Test.thy",
11.80 + ("Test",
11.81 ["linear","univariate","equation","test"],
11.82 ["Test","solve_linear"]))];
11.83 Iterator 1;
11.84 @@ -442,7 +442,7 @@
11.85 states:=[];
11.86 CalcTree
11.87 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.88 - ("Test.thy",
11.89 + ("Test",
11.90 ["sqroot-test","univariate","equation","test"],
11.91 ["Test","squ-equ-test-subpbl1"]))];
11.92 Iterator 1;
11.93 @@ -474,7 +474,7 @@
11.94 states:=[];
11.95 CalcTree
11.96 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.97 - ("Test.thy",
11.98 + ("Test",
11.99 ["sqroot-test","univariate","equation","test"],
11.100 ["Test","squ-equ-test-subpbl1"]))];
11.101 Iterator 1;
11.102 @@ -488,7 +488,7 @@
11.103 states:=[];
11.104 CalcTree
11.105 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
11.106 - ("Test.thy",
11.107 + ("Test",
11.108 ["linear","univariate","equation","test"],
11.109 ["Test","solve_linear"]))];
11.110 Iterator 1;
11.111 @@ -530,7 +530,7 @@
11.112 states:=[];
11.113 CalcTree
11.114 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.115 - ("Test.thy",
11.116 + ("Test",
11.117 ["sqroot-test","univariate","equation","test"],
11.118 ["Test","squ-equ-test-subpbl1"]))];
11.119 Iterator 1; moveActiveRoot 1;
11.120 @@ -560,7 +560,7 @@
11.121 states:=[];
11.122 CalcTree
11.123 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.124 - ("Test.thy",
11.125 + ("Test",
11.126 ["sqroot-test","univariate","equation","test"],
11.127 ["Test","squ-equ-test-subpbl1"]))];
11.128 Iterator 1; moveActiveRoot 1;
11.129 @@ -593,7 +593,7 @@
11.130 states:=[];
11.131 CalcTree
11.132 [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
11.133 - ("RatEq.thy", ["univariate","equation"], ["no_met"]))];
11.134 + ("RatEq", ["univariate","equation"], ["no_met"]))];
11.135 Iterator 1;
11.136 moveActiveRoot 1;
11.137 fetchProposedTactic 1;
11.138 @@ -607,7 +607,7 @@
11.139 setNextTactic 1 (Add_Find "solutions L");
11.140 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.141 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
11.142 - setNextTactic 1 (Specify_Theory "RatEq.thy");
11.143 + setNextTactic 1 (Specify_Theory "RatEq");
11.144 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.145 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
11.146 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.147 @@ -622,7 +622,7 @@
11.148 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
11.149 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.150 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
11.151 - setNextTactic 1 (Subproblem ("PolyEq.thy", ["normalize","polynomial",
11.152 + setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
11.153 "univariate","equation"]));
11.154 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.155 setNextTactic 1 (Model_Problem );
11.156 @@ -636,7 +636,7 @@
11.157 setNextTactic 1 (Add_Find "solutions x_i");
11.158 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.159 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
11.160 - setNextTactic 1 (Specify_Theory "PolyEq.thy");
11.161 + setNextTactic 1 (Specify_Theory "PolyEq");
11.162 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.163 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
11.164 "univariate","equation"]);
11.165 @@ -650,7 +650,7 @@
11.166 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
11.167 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.168 (* __________ for "16 + 12 * x = 0"*)
11.169 - setNextTactic 1 (Subproblem ("PolyEq.thy",
11.170 + setNextTactic 1 (Subproblem ("PolyEq",
11.171 ["degree_1","polynomial","univariate","equation"]));
11.172 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.173 setNextTactic 1 (Model_Problem );
11.174 @@ -664,7 +664,7 @@
11.175 setNextTactic 1 (Add_Find "solutions x_i");
11.176 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.177 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
11.178 - setNextTactic 1 (Specify_Theory "PolyEq.thy");
11.179 + setNextTactic 1 (Specify_Theory "PolyEq");
11.180 (*------------- some trials in the problem-hierarchy ---------------*)
11.181 setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
11.182 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
11.183 @@ -796,7 +796,7 @@
11.184 (*WN050904 the fetchProposedTactic's below may not have worked like that
11.185 before, too, because there was no check*)
11.186 fetchProposedTactic 1;
11.187 - setNextTactic 1 (Specify_Theory "PolyEq.thy");
11.188 + setNextTactic 1 (Specify_Theory "PolyEq");
11.189 autoCalculate 1 (Step 1);
11.190
11.191 fetchProposedTactic 1;
11.192 @@ -824,7 +824,7 @@
11.193 DEconstrCalcTree 1;
11.194 CalcTree
11.195 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.196 - ("Test.thy",
11.197 + ("Test",
11.198 ["sqroot-test","univariate","equation","test"],
11.199 ["Test","squ-equ-test-subpbl1"]))];
11.200 Iterator 1;
11.201 @@ -835,7 +835,7 @@
11.202 [Given ["equality (x+1=2)", "solveFor x"],
11.203 Find ["solutions L"](*,Relate []*)],
11.204 Pbl,
11.205 - ("Test.thy",
11.206 + ("Test",
11.207 ["sqroot-test","univariate","equation","test"],
11.208 ["Test","squ-equ-test-subpbl1"]));
11.209 resetCalcHead 1;
11.210 @@ -860,7 +860,7 @@
11.211 "interval {x::real. 0 <= x & x <= pi}",
11.212 "errorBound (eps=(0::real))"]
11.213 (*specifying is not interesting for this example*)
11.214 - val spec = ("DiffApp.thy", ["maximum_of","function"],
11.215 + val spec = ("DiffApp", ["maximum_of","function"],
11.216 ["DiffApp","max_by_calculus"]);
11.217 (*the empty model with descriptions for user-guidance by Model_Problem*)
11.218 val empty_model = [Given ["fixedValues []"],
11.219 @@ -913,20 +913,20 @@
11.220 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
11.221 Relate ["relations [A=a*b, \
11.222 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
11.223 - ("DiffApp.thy", ["e_pblID"], ["e_metID"]));
11.224 + ("DiffApp", ["e_pblID"], ["e_metID"]));
11.225 modifyCalcHead 1 (([],Pbl), "not used here",
11.226 [Given ["fixedValues [r=Arbfix]"],
11.227 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
11.228 Relate ["relations [A=a*b, \
11.229 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
11.230 - ("DiffApp.thy", ["maximum_of","function"],
11.231 + ("DiffApp", ["maximum_of","function"],
11.232 ["e_metID"]));
11.233 modifyCalcHead 1 (([],Pbl), "not used here",
11.234 [Given ["fixedValues [r=Arbfix]"],
11.235 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
11.236 Relate ["relations [A=a*b, \
11.237 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
11.238 - ("DiffApp.thy", ["maximum_of","function"],
11.239 + ("DiffApp", ["maximum_of","function"],
11.240 ["DiffApp","max_by_calculus"]));
11.241 (*this final calcHead now has STATUS 'complete' !*)
11.242 DEconstrCalcTree 1;
11.243 @@ -944,7 +944,7 @@
11.244 [Given ["equality (1+-1*2+x=0)", "solveFor x"],
11.245 Find ["solutions L"]],
11.246 Pbl,
11.247 - ("Test.thy", ["linear","univariate","equation","test"],
11.248 + ("Test", ["linear","univariate","equation","test"],
11.249 ["Test","solve_linear"]));
11.250 autoCalculate 1 CompleteCalc;
11.251 refFormula 1 (get_pos 1 1);
11.252 @@ -980,7 +980,7 @@
11.253 states:=[];
11.254 CalcTree
11.255 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.256 - ("Test.thy",
11.257 + ("Test",
11.258 ["sqroot-test","univariate","equation","test"],
11.259 ["Test","squ-equ-test-subpbl1"]))];
11.260 Iterator 1;
11.261 @@ -1018,7 +1018,7 @@
11.262 states:=[];
11.263 CalcTree
11.264 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.265 - ("Test.thy",
11.266 + ("Test",
11.267 ["sqroot-test","univariate","equation","test"],
11.268 ["Test","squ-equ-test-subpbl1"]))];
11.269 Iterator 1; moveActiveRoot 1;
11.270 @@ -1050,7 +1050,7 @@
11.271 CalcTree
11.272 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
11.273 "solveFor x","solutions L"],
11.274 - ("RatEq.thy",["univariate","equation"],["no_met"]))];
11.275 + ("RatEq",["univariate","equation"],["no_met"]))];
11.276 Iterator 1; moveActiveRoot 1;
11.277 autoCalculate 1 CompleteCalc;
11.278 val ((pt,_),_) = get_calc 1;
11.279 @@ -1070,7 +1070,7 @@
11.280 states:=[];
11.281 CalcTree (*start of calculation, return No.1*)
11.282 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
11.283 - ("Test.thy",
11.284 + ("Test",
11.285 ["linear","univariate","equation","test"],
11.286 ["Test","solve_linear"]))];
11.287 Iterator 1; moveActiveRoot 1;
11.288 @@ -1088,7 +1088,7 @@
11.289 autoCalculate 1 (Step 1);
11.290 autoCalculate 1 (Step 1);
11.291
11.292 - setNextTactic 1 (Specify_Theory "Test.thy");
11.293 + setNextTactic 1 (Specify_Theory "Test");
11.294 fetchProposedTactic 1;
11.295 autoCalculate 1 (Step 1);
11.296
11.297 @@ -1120,7 +1120,7 @@
11.298 states:=[];
11.299 CalcTree
11.300 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.301 - ("Test.thy",
11.302 + ("Test",
11.303 ["sqroot-test","univariate","equation","test"],
11.304 ["Test","squ-equ-test-subpbl1"]))];
11.305 Iterator 1;
11.306 @@ -1145,7 +1145,7 @@
11.307 states:=[];
11.308 CalcTree
11.309 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.310 - ("Test.thy",
11.311 + ("Test",
11.312 ["sqroot-test","univariate","equation","test"],
11.313 ["Test","squ-equ-test-subpbl1"]))];
11.314 Iterator 1;
11.315 @@ -1170,7 +1170,7 @@
11.316 states:=[];
11.317 CalcTree
11.318 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.319 - ("Test.thy",
11.320 + ("Test",
11.321 ["sqroot-test","univariate","equation","test"],
11.322 ["Test","squ-equ-test-subpbl1"]))];
11.323 Iterator 1;
11.324 @@ -1197,7 +1197,7 @@
11.325 states:=[];
11.326 CalcTree
11.327 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.328 - ("Test.thy",
11.329 + ("Test",
11.330 ["sqroot-test","univariate","equation","test"],
11.331 ["Test","squ-equ-test-subpbl1"]))];
11.332 Iterator 1;
11.333 @@ -1221,7 +1221,7 @@
11.334 states:=[];
11.335 CalcTree
11.336 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.337 - ("Test.thy",
11.338 + ("Test",
11.339 ["sqroot-test","univariate","equation","test"],
11.340 ["Test","squ-equ-test-subpbl1"]))];
11.341 Iterator 1;
11.342 @@ -1244,7 +1244,7 @@
11.343 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
11.344 CalcTree
11.345 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.346 - ("Test.thy",
11.347 + ("Test",
11.348 ["sqroot-test","univariate","equation","test"],
11.349 ["Test","squ-equ-test-subpbl1"]))];
11.350 Iterator 2;
11.351 @@ -1270,7 +1270,7 @@
11.352 states:=[];
11.353 CalcTree
11.354 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.355 - ("Test.thy",
11.356 + ("Test",
11.357 ["sqroot-test","univariate","equation","test"],
11.358 ["Test","squ-equ-test-subpbl1"]))];
11.359 Iterator 1;
11.360 @@ -1307,7 +1307,7 @@
11.361 states:=[];
11.362 CalcTree
11.363 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.364 - ("Test.thy",
11.365 + ("Test",
11.366 ["sqroot-test","univariate","equation","test"],
11.367 ["Test","squ-equ-test-subpbl1"]))];
11.368 Iterator 1;
11.369 @@ -1342,7 +1342,7 @@
11.370 states:=[];
11.371 CalcTree
11.372 [(["equality (x+1=2)", "solveFor x","solutions L"],
11.373 - ("Test.thy",
11.374 + ("Test",
11.375 ["sqroot-test","univariate","equation","test"],
11.376 ["Test","squ-equ-test-subpbl1"]))];
11.377 Iterator 1;
12.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Oct 11 12:55:40 2010 +0200
12.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Oct 11 13:31:22 2010 +0200
12.3 @@ -28,7 +28,7 @@
12.4 states := [];
12.5 CalcTree
12.6 [(["equality (x+1=2)", "solveFor x","solutions L"],
12.7 - ("Test.thy",
12.8 + ("Test",
12.9 ["sqroot-test","univariate","equation","test"],
12.10 ["Test","squ-equ-test-subpbl1"]))];
12.11 Iterator 1;
12.12 @@ -73,7 +73,7 @@
12.13 "interval {x::real. 0 <= x & x <= pi}",
12.14 "errorBound (eps=(0::real))"];
12.15 val (dI',pI',mI') =
12.16 - ("DiffApp.thy",["maximum_of","function"],
12.17 + ("DiffApp",["maximum_of","function"],
12.18 ["DiffApp","max_by_calculus"]);
12.19 val c = []:cid;
12.20
12.21 @@ -167,7 +167,7 @@
12.22 "interval {x::real. 0 <= x & x <= pi}",
12.23 "errorBound (eps=(0::real))"];
12.24 val (dI',pI',mI') =
12.25 - ("DiffApp.thy",["maximum_of","function"],
12.26 + ("DiffApp",["maximum_of","function"],
12.27 ["DiffApp","max_by_calculus"]);
12.28 val c = []:cid;
12.29 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
12.30 @@ -210,7 +210,7 @@
12.31 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.32 ------------------------------ FIXXXXME.meNEW !!! ---*)
12.33
12.34 -(*val nxt = Specify_Theory "DiffApp.thy" : tac*)
12.35 +(*val nxt = Specify_Theory "DiffApp" : tac*)
12.36
12.37 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
12.38
12.39 @@ -220,7 +220,7 @@
12.40
12.41 val nxt = tac2tac_ pt p nxt;
12.42 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.43 -(*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
12.44 +(*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
12.45
12.46 val nxt = tac2tac_ pt p nxt;
12.47 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.48 @@ -236,7 +236,7 @@
12.49
12.50 val nxt = tac2tac_ pt p nxt;
12.51 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.52 -(*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
12.53 +(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
12.54 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
12.55 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
12.56
12.57 @@ -256,7 +256,7 @@
12.58 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.59 (*val nxt = Specify_Theory "e_domID" : tac*)
12.60
12.61 -val nxt = Specify_Theory "DiffApp.thy";
12.62 +val nxt = Specify_Theory "DiffApp";
12.63 val nxt = tac2tac_ pt p nxt;
12.64 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.65 (*val nxt = Specify_Problem ["e_pblID"] : tac*)
12.66 @@ -315,13 +315,13 @@
12.67 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
12.68 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
12.69 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
12.70 -if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
12.71 +if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
12.72 then error "test specify, fmz <> []: nxt <> Add_Relation.."
12.73 else ();
12.74 *)
12.75
12.76 (* 2.4.00 nach Transfer specify -> hard_gen
12.77 -val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
12.78 +val nxt = Apply_Method ("DiffApp","max_by_calculus");
12.79 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
12.80 (*val nxt = Empty_Tac : tac*)
12.81
12.82 @@ -602,7 +602,7 @@
12.83 {env = None, fmz =
12.84 (["functionTerm (x^^^2 + 1)", "integrateBy x",
12.85 "antiDerivative FF"],
12.86 - ("Integrate.thy", ["integrate", "function"],
12.87 + ("Integrate", ["integrate", "function"],
12.88 ["diff", "integration"])),
12.89 loc =
12.90 (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
12.91 @@ -624,7 +624,7 @@
12.92 (3, [1], "#Find",
12.93 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
12.94 [Free ("FF", "RealDef.real")])],
12.95 - ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
12.96 + ("Integrate", ["integrate", "function"], ["diff", "integration"]),
12.97 Const ("Integrate.Integrate",
12.98 "(RealDef.real, RealDef.real) * => RealDef.real") $
12.99 (Const ("Pair",
12.100 @@ -662,7 +662,7 @@
12.101 {env = None, fmz =
12.102 (["functionTerm (x^^^2 + 1)", "integrateBy x",
12.103 "antiDerivative FF"],
12.104 - ("Integrate.thy", ["integrate", "function"],
12.105 + ("Integrate", ["integrate", "function"],
12.106 ["diff", "integration"])),
12.107 loc =
12.108 (Some
12.109 @@ -697,7 +697,7 @@
12.110 (3, [1], "#Find",
12.111 Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
12.112 [Free ("FF", "RealDef.real")])],
12.113 - ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
12.114 + ("Integrate", ["integrate", "function"], ["diff", "integration"]),
12.115 Const ("Integrate.Integrate",
12.116 "(RealDef.real, RealDef.real) * => RealDef.real") $
12.117 (Const ("Pair",
13.1 --- a/test/Tools/isac/Interpret/ctree.sml Mon Oct 11 12:55:40 2010 +0200
13.2 +++ b/test/Tools/isac/Interpret/ctree.sml Mon Oct 11 13:31:22 2010 +0200
13.3 @@ -67,7 +67,7 @@
13.4 val fmz = ["equality (x+1=2)",
13.5 "solveFor x","solutions L"];
13.6 val (dI',pI',mI') =
13.7 - ("Test.thy",["sqroot-test","univariate","equation","test"],
13.8 + ("Test",["sqroot-test","univariate","equation","test"],
13.9 ["Test","squ-equ-test-subpbl1"]);
13.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
13.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.12 @@ -308,7 +308,7 @@
13.13 val fmz = ["equality (x+1=2)",
13.14 "solveFor x","solutions L"];
13.15 val (dI',pI',mI') =
13.16 - ("Test.thy",["sqroot-test","univariate","equation","test"],
13.17 + ("Test",["sqroot-test","univariate","equation","test"],
13.18 ["Test","squ-equ-test-subpbl1"]);
13.19 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
13.20 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.21 @@ -350,7 +350,7 @@
13.22 states:=[];
13.23 CalcTree
13.24 [(["equality (x+1=2)", "solveFor x","solutions L"],
13.25 - ("Test.thy",
13.26 + ("Test",
13.27 ["sqroot-test","univariate","equation","test"],
13.28 ["Test","squ-equ-test-subpbl1"]))];
13.29 Iterator 1; moveActiveRoot 1;
13.30 @@ -416,7 +416,7 @@
13.31 val fmz = ["equality (x+1=2)",
13.32 "solveFor x","solutions L"];
13.33 val (dI',pI',mI') =
13.34 - ("Test.thy",["sqroot-test","univariate","equation","test"],
13.35 + ("Test",["sqroot-test","univariate","equation","test"],
13.36 ["Test","squ-equ-test-subpbl1"]);
13.37 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
13.38 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.39 @@ -517,7 +517,7 @@
13.40 states:=[];
13.41 CalcTree
13.42 [(["equality (x+1=2)", "solveFor x","solutions L"],
13.43 - ("Test.thy",
13.44 + ("Test",
13.45 ["sqroot-test","univariate","equation","test"],
13.46 ["Test","squ-equ-test-subpbl1"]))];
13.47 Iterator 1; moveActiveRoot 1;
13.48 @@ -554,7 +554,7 @@
13.49 states := [];
13.50 CalcTree (*start of calculation, return No.1*)
13.51 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
13.52 - ("Test.thy",
13.53 + ("Test",
13.54 ["linear","univariate","equation","test"],
13.55 ["Test","solve_linear"]))];
13.56 Iterator 1; moveActiveRoot 1;
13.57 @@ -601,7 +601,7 @@
13.58 states:=[];
13.59 CalcTree
13.60 [(["equality (x+1=2)", "solveFor x","solutions L"],
13.61 - ("Test.thy",
13.62 + ("Test",
13.63 ["sqroot-test","univariate","equation","test"],
13.64 ["Test","squ-equ-test-subpbl1"]))];
13.65 Iterator 1; moveActiveRoot 1;
13.66 @@ -635,7 +635,7 @@
13.67 states:=[];
13.68 CalcTree
13.69 [(["equality (x+1=2)", "solveFor x","solutions L"],
13.70 - ("Test.thy",
13.71 + ("Test",
13.72 ["sqroot-test","univariate","equation","test"],
13.73 ["Test","squ-equ-test-subpbl1"]))];
13.74 Iterator 1; moveActiveRoot 1;
13.75 @@ -671,7 +671,7 @@
13.76 CalcTree
13.77 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
13.78 "solveFor x","solutions L"],
13.79 - ("RatEq.thy",["univariate","equation"],["no_met"]))];
13.80 + ("RatEq",["univariate","equation"],["no_met"]))];
13.81 Iterator 1; moveActiveRoot 1;
13.82 autoCalculate 1 CompleteCalc;
13.83
13.84 @@ -853,7 +853,7 @@
13.85 CalcTree
13.86 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
13.87 "solveFor x","solutions L"],
13.88 - ("RatEq.thy",["univariate","equation"],["no_met"]))];
13.89 + ("RatEq",["univariate","equation"],["no_met"]))];
13.90 Iterator 1; moveActiveRoot 1;
13.91 autoCalculate 1 CompleteCalc;
13.92 val ((pt,_),_) = get_calc 1;
13.93 @@ -867,7 +867,7 @@
13.94 case (term2str form, tac, terms2strs asm) of
13.95 ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
13.96 Subproblem
13.97 - ("PolyEq.thy",
13.98 + ("PolyEq",
13.99 ["normalize", "polynomial", "univariate", "equation"]),
13.100 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
13.101 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
13.102 @@ -877,7 +877,7 @@
13.103 case (term2str form, tac, terms2strs asm) of
13.104 ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
13.105 *)Subproblem
13.106 - ("PolyEq.thy",
13.107 + ("PolyEq",
13.108 ["normalize", "polynomial", "univariate", "equation"]),
13.109 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
13.110 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
13.111 @@ -892,7 +892,7 @@
13.112 states:=[];
13.113 CalcTree
13.114 [(["equality (x+1=2)", "solveFor x","solutions L"],
13.115 - ("Test.thy",
13.116 + ("Test",
13.117 ["sqroot-test","univariate","equation","test"],
13.118 ["Test","squ-equ-test-subpbl1"]))];
13.119 Iterator 1; moveActiveRoot 1;
13.120 @@ -923,7 +923,7 @@
13.121 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
13.122 case (term2str form, tac, terms2strs asm) of
13.123 ("-1 + x = 0",
13.124 - Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
13.125 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
13.126 []) => ()
13.127 | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
13.128
13.129 @@ -971,7 +971,7 @@
13.130 states:=[];
13.131 CalcTree
13.132 [(["equality (x+1=2)", "solveFor x","solutions L"],
13.133 - ("Test.thy",
13.134 + ("Test",
13.135 ["sqroot-test","univariate","equation","test"],
13.136 ["Test","squ-equ-test-subpbl1"]))];
13.137 Iterator 1; moveActiveRoot 1;
14.1 --- a/test/Tools/isac/Interpret/inform.sml Mon Oct 11 12:55:40 2010 +0200
14.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon Oct 11 13:31:22 2010 +0200
14.3 @@ -51,7 +51,7 @@
14.4
14.5 states:=[];
14.6 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.7 - ("Test.thy",
14.8 + ("Test",
14.9 ["sqroot-test","univariate","equation","test"],
14.10 ["Test","squ-equ-test-subpbl1"]))];
14.11 Iterator 1; moveActiveRoot 1;
14.12 @@ -124,7 +124,7 @@
14.13 "--------- appendFormula: on Frm + equ_nrls ----------------------";
14.14 states:=[];
14.15 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.16 - ("Test.thy",
14.17 + ("Test",
14.18 ["sqroot-test","univariate","equation","test"],
14.19 ["Test","squ-equ-test-subpbl1"]))];
14.20 Iterator 1; moveActiveRoot 1;
14.21 @@ -161,7 +161,7 @@
14.22 "--------- appendFormula: on Res + NO deriv ----------------------";
14.23 states:=[];
14.24 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.25 - ("Test.thy",
14.26 + ("Test",
14.27 ["sqroot-test","univariate","equation","test"],
14.28 ["Test","squ-equ-test-subpbl1"]))];
14.29 Iterator 1; moveActiveRoot 1;
14.30 @@ -192,7 +192,7 @@
14.31 "--------- appendFormula: on Res + late deriv --------------------";
14.32 states:=[];
14.33 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.34 - ("Test.thy",
14.35 + ("Test",
14.36 ["sqroot-test","univariate","equation","test"],
14.37 ["Test","squ-equ-test-subpbl1"]))];
14.38 Iterator 1; moveActiveRoot 1;
14.39 @@ -223,7 +223,7 @@
14.40 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
14.41 states:=[];
14.42 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.43 - ("Test.thy",
14.44 + ("Test",
14.45 ["sqroot-test","univariate","equation","test"],
14.46 ["Test","squ-equ-test-subpbl1"]))];
14.47 Iterator 1; moveActiveRoot 1;
14.48 @@ -249,7 +249,7 @@
14.49 "--------- replaceFormula: on Res + = ----------------------------";
14.50 states:=[];
14.51 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.52 - ("Test.thy",
14.53 + ("Test",
14.54 ["sqroot-test","univariate","equation","test"],
14.55 ["Test","squ-equ-test-subpbl1"]))];
14.56 Iterator 1; moveActiveRoot 1;
14.57 @@ -275,7 +275,7 @@
14.58 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
14.59 states:=[];
14.60 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.61 - ("Test.thy",
14.62 + ("Test",
14.63 ["sqroot-test","univariate","equation","test"],
14.64 ["Test","squ-equ-test-subpbl1"]))];
14.65 Iterator 1; moveActiveRoot 1;
14.66 @@ -300,7 +300,7 @@
14.67 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
14.68 states:=[];
14.69 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.70 - ("Test.thy",
14.71 + ("Test",
14.72 ["sqroot-test","univariate","equation","test"],
14.73 ["Test","squ-equ-test-subpbl1"]))];
14.74 Iterator 1; moveActiveRoot 1;
14.75 @@ -324,7 +324,7 @@
14.76 "--------- replaceFormula: cut calculation -----------------------";
14.77 states:=[];
14.78 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.79 - ("Test.thy",
14.80 + ("Test",
14.81 ["sqroot-test","univariate","equation","test"],
14.82 ["Test","squ-equ-test-subpbl1"]))];
14.83 Iterator 1; moveActiveRoot 1;
14.84 @@ -360,7 +360,7 @@
14.85 "interval {x::real. 0 <= x & x <= pi}",
14.86 "errorBound (eps=(0::real))"]
14.87 (*specifying is not interesting for this example*)
14.88 - val spec = ("DiffApp.thy", ["maximum_of","function"],
14.89 + val spec = ("DiffApp", ["maximum_of","function"],
14.90 ["DiffApp","max_by_calculus"]);
14.91 (*the empty model with descriptions for user-guidance by Model_Problem*)
14.92 val empty_model = [Given ["fixedValues []"],
14.93 @@ -422,7 +422,7 @@
14.94 "--------- syntax error ------------------------------------------";
14.95 states:=[];
14.96 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
14.97 - ("Test.thy",
14.98 + ("Test",
14.99 ["sqroot-test","univariate","equation","test"],
14.100 ["Test","squ-equ-test-subpbl1"]))];
14.101 Iterator 1; moveActiveRoot 1;
14.102 @@ -472,7 +472,7 @@
14.103 "--------- inform [rational,simplification] ----------------------";
14.104 states:=[];
14.105 CalcTree [(["TERM (4/x - 3/y - 1)", "normalform N"],
14.106 - ("Rational.thy",["rational","simplification"],
14.107 + ("Rational",["rational","simplification"],
14.108 ["simplification","of_rationals"]))];
14.109 Iterator 1; moveActiveRoot 1;
14.110 autoCalculate 1 CompleteCalcHead;
15.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Oct 11 12:55:40 2010 +0200
15.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon Oct 11 13:31:22 2010 +0200
15.3 @@ -23,7 +23,7 @@
15.4 states:=[];
15.5 CalcTree
15.6 [(["equality (x+1=2)", "solveFor x","solutions L"],
15.7 - ("Test.thy",
15.8 + ("Test",
15.9 ["sqroot-test","univariate","equation","test"],
15.10 ["Test","squ-equ-test-subpbl1"]))];
15.11 Iterator 1;
15.12 @@ -58,7 +58,7 @@
15.13 states:=[];
15.14 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
15.15 "solveFor x", "solutions L"],
15.16 - ("RatEq.thy",["univariate","equation"],["no_met"]))];
15.17 + ("RatEq",["univariate","equation"],["no_met"]))];
15.18 Iterator 1;
15.19 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
15.20
16.1 --- a/test/Tools/isac/Interpret/me.sml Mon Oct 11 12:55:40 2010 +0200
16.2 +++ b/test/Tools/isac/Interpret/me.sml Mon Oct 11 13:31:22 2010 +0200
16.3 @@ -32,7 +32,7 @@
16.4 CalcTree
16.5 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
16.6 "solveFor x","solutions L"],
16.7 - ("RatEq.thy",["univariate","equation"],["no_met"]))];
16.8 + ("RatEq",["univariate","equation"],["no_met"]))];
16.9 Iterator 1; moveActiveRoot 1;
16.10 autoCalculate 1 CompleteCalc;
16.11
16.12 @@ -226,7 +226,7 @@
16.13 CalcTree
16.14 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
16.15 "solveFor x","solutions L"],
16.16 - ("RatEq.thy",["univariate","equation"],["no_met"]))];
16.17 + ("RatEq",["univariate","equation"],["no_met"]))];
16.18 Iterator 1; moveActiveRoot 1;
16.19 autoCalculate 1 CompleteCalc;
16.20 val ((pt,_),_) = get_calc 1;
16.21 @@ -338,7 +338,7 @@
16.22 val c = [];
16.23 val (p,_,f,nxt,_,pt) = CalcTreeTEST
16.24 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
16.25 - ("Test.thy",
16.26 + ("Test",
16.27 ["linear","univariate","equation","test"],
16.28 ["Test","solve_linear"]))];
16.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.30 @@ -374,7 +374,7 @@
16.31 states:=[];
16.32 CalcTree (*start of calculation, return No.1*)
16.33 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
16.34 - ("Test.thy",
16.35 + ("Test",
16.36 ["linear","univariate","equation","test"],
16.37 ["Test","solve_linear"]))];
16.38 Iterator 1; moveActiveRoot 1;
16.39 @@ -421,7 +421,7 @@
16.40 "interval {x::real. 0 <= x & x <= 2*r}",
16.41 "interval {x::real. 0 <= x & x <= pi}",
16.42 "errorBound (eps=(0::real))"],
16.43 - ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
16.44 + ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
16.45 )];
16.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.47 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.48 @@ -430,7 +430,7 @@
16.49 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
16.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.52 - (*nxt = Specify_Theory "DiffApp.thy"*)
16.53 + (*nxt = Specify_Theory "DiffApp"*)
16.54 val (oris, _, _) = get_obj g_origin pt (fst p);
16.55 writeln (oris2str oris);
16.56 (*[
16.57 @@ -487,7 +487,7 @@
16.58 "interval {x::real. 0 <= x & x <= 2*r}",
16.59 "interval {x::real. 0 <= x & x <= pi}",
16.60 "errorBound (eps=(0::real))"],
16.61 - ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
16.62 + ("DiffApp",["maximum_of","function"],["DiffApp","max_by_calculus"])
16.63 )];
16.64 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.65 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.1 --- a/test/Tools/isac/Interpret/ptyps.sml Mon Oct 11 12:55:40 2010 +0200
17.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Mon Oct 11 13:31:22 2010 +0200
17.3 @@ -341,7 +341,7 @@
17.4 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
17.5 val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",
17.6 "errorBound (eps=0)","solutions L"];
17.7 -val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
17.8 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
17.9 ["Test","squ-equ-test-subpbl1"]);
17.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
17.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.12 @@ -374,7 +374,7 @@
17.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.14 (*("Specify_Problem", Specify_Problem ["normalize", "univariate", ...])*)
17.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.16 -(*nxt = ("Specify_Theory", Specify_Theory "Test.thy")*)
17.17 +(*nxt = ("Specify_Theory", Specify_Theory "Test")*)
17.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.19 (*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
17.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.21 @@ -384,7 +384,7 @@
17.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.23 (*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
17.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.25 -(*Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]*)
17.26 +(*Subproblem ("Test", ["linear", "univariate", "equation", "test"]*)
17.27
17.28 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.29 (*nxt = Model_Problem ["linear","univariate","equation","test"]*)
18.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Oct 11 12:55:40 2010 +0200
18.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Mon Oct 11 13:31:22 2010 +0200
18.3 @@ -100,7 +100,7 @@
18.4 "----------- fun thy_containing_thm ------------------------------";
18.5 "----------- fun thy_containing_thm ------------------------------";
18.6 "----------- fun thy_containing_thm ------------------------------";
18.7 -val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy));
18.8 +val (str, (thy', thy)) = ("real_diff_minus",("Root", Root.thy));
18.9 if thy_contains_thm str ("XXX",thy) then ()
18.10 else error "rewtools.sml: NOT thy_contains_thm \
18.11 \(real_diff_minus,(Root.thy,.";
18.12 @@ -110,7 +110,7 @@
18.13 val startsearch = dropuntil ((curry op= thy') o
18.14 (#1:theory' * theory -> theory'))
18.15 (rev (!theory'));
18.16 -if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then ()
18.17 +if thy_containing_thm thy' str = ("IsacKnowledge", "Root") then ()
18.18 else error "rewtools.sml: NOT thy_containin_thm \
18.19 \(real_diff_minus,(Root.thy,.";
18.20
18.21 @@ -118,20 +118,20 @@
18.22 if thy_contains_thm str ("XXX",Poly.thy) then ()
18.23 else error "rewtools.sml: NOT thy_contains_thm \
18.24 \(real_diff_minus,(Poly.thy,.";
18.25 -if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then ()
18.26 +if thy_containing_thm "LinEq" str = ("IsacKnowledge", "Poly") then ()
18.27 else error "rewtools.sml: NOT thy_containing_thm \
18.28 \(real_diff_minus,(Poly.thy,.";
18.29
18.30 "----- second test -------------------------------";
18.31 show_thes();
18.32 (*args vor thy_containing_thm...*)
18.33 -val (thy',str) = ("Test.thy", "radd_commute");
18.34 +val (thy',str) = ("Test", "radd_commute");
18.35 val startsearch = dropuntil ((curry op= thy') o
18.36 (#1:theory' * theory -> theory'))
18.37 (rev (!theory'));
18.38 length (!theory');
18.39 length startsearch;
18.40 -if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then ()
18.41 +if thy_containing_thm thy' str = ("IsacKnowledge", "Test") then ()
18.42 else error "rewtools.sml: diff.behav. in \
18.43 \thy_containing_thm Test radd_commute";
18.44
18.45 @@ -139,7 +139,7 @@
18.46 "----------- fun thy_containing_rls ------------------------------";
18.47 "----------- fun thy_containing_rls ------------------------------";
18.48 "----------- fun thy_containing_rls ------------------------------";
18.49 -val thy' = "Biegelinie.thy";
18.50 +val thy' = "Biegelinie";
18.51 val dropthys = takewhile [] (not o (curry op= thy') o
18.52 (#1:theory' * theory -> theory'))
18.53 (rev (!theory'));
18.54 @@ -169,14 +169,14 @@
18.55 | _ => error ("thy_containing_rls : rls '"^str^
18.56 "' not in !rulset' und thy '"^thy'^"'");
18.57
18.58 -if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then ()
18.59 +if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly") then ()
18.60 else error "rewtools.sml: diff.behav. in thy_containing_rls 3";
18.61
18.62
18.63 "----------- fun thy_containing_cal ------------------------------";
18.64 "----------- fun thy_containing_cal ------------------------------";
18.65 "----------- fun thy_containing_cal ------------------------------";
18.66 -val thy' = "Atools.thy";
18.67 +val thy' = "Atools";
18.68 val dropthys = takewhile [] (not o (curry op= thy') o
18.69 (#1:theory' * theory -> theory'))
18.70 (rev (!theory'));
18.71 @@ -197,7 +197,7 @@
18.72 states:=[];
18.73 CalcTree
18.74 [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
18.75 - ("Integrate.thy",["integrate","function"],
18.76 + ("Integrate",["integrate","function"],
18.77 ["diff","integration"]))];
18.78 Iterator 1;
18.79 moveActiveRoot 1;
18.80 @@ -218,7 +218,7 @@
18.81 states:=[];
18.82 CalcTree (*start of calculation, return No.1*)
18.83 [(["equality (x+1=2)", "solveFor x","solutions L"],
18.84 - ("Test.thy",
18.85 + ("Test",
18.86 ["sqroot-test","univariate","equation","test"],
18.87 ["Test","squ-equ-test-subpbl1"]))];
18.88 Iterator 1; moveActiveRoot 1;
18.89 @@ -349,7 +349,7 @@
18.90 states:=[];
18.91 CalcTree (*start of calculation, return No.1*)
18.92 [(["equality (x+1=2)", "solveFor x","solutions L"],
18.93 - ("Test.thy",
18.94 + ("Test",
18.95 ["sqroot-test","univariate","equation","test"],
18.96 ["Test","squ-equ-test-subpbl1"]))];
18.97 Iterator 1; moveActiveRoot 1;
18.98 @@ -397,7 +397,7 @@
18.99 states:=[];
18.100 CalcTree
18.101 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
18.102 - ("Test.thy",
18.103 + ("Test",
18.104 ["linear","univariate","equation","test"],
18.105 ["Test","solve_linear"]))];
18.106 Iterator 1; moveActiveRoot 1;
18.107 @@ -419,7 +419,7 @@
18.108 states:=[];
18.109 CalcTree
18.110 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
18.111 - ("Test.thy",
18.112 + ("Test",
18.113 ["linear","univariate","equation","test"],
18.114 ["Test","solve_linear"]))];
18.115 Iterator 1; moveActiveRoot 1;
18.116 @@ -451,7 +451,7 @@
18.117 applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
18.118 "- compose stac as done in | appy (*leaf*) by handle_leaf";
18.119 val (th, sr, E, a, v, t) =
18.120 - ("Biegelinie.thy",
18.121 + ("Biegelinie",
18.122 (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
18.123 [(str2term "q__::bool", str2term "q x = q_0")],
18.124 SOME (str2term "q x = q_0"),
18.125 @@ -485,7 +485,7 @@
18.126 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
18.127 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
18.128 "FunktionsVariable x"],
18.129 - ("Biegelinie.thy",
18.130 + ("Biegelinie",
18.131 ["MomentBestimmte","Biegelinien"],
18.132 ["IntegrierenUndKonstanteBestimmen"]))];
18.133 moveActiveRoot 1;
19.1 --- a/test/Tools/isac/Interpret/script.sml Mon Oct 11 12:55:40 2010 +0200
19.2 +++ b/test/Tools/isac/Interpret/script.sml Mon Oct 11 13:31:22 2010 +0200
19.3 @@ -85,7 +85,7 @@
19.4 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
19.5 "FunktionsVariable x"];
19.6 val (dI',pI',mI') =
19.7 - ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
19.8 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
19.9 ["IntegrierenUndKonstanteBestimmen"]);
19.10 val p = e_pos'; val c = [];
19.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.12 @@ -160,7 +160,7 @@
19.13 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
19.14 "FunktionsVariable x"];
19.15 val (dI',pI',mI') =
19.16 - ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
19.17 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
19.18 ["IntegrierenUndKonstanteBestimmen"]);
19.19 val p = e_pos'; val c = [];
19.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.21 @@ -221,7 +221,7 @@
19.22 states:=[];
19.23 CalcTree
19.24 [(["equality (x+1=2)", "solveFor x","solutions L"],
19.25 - ("Test.thy",
19.26 + ("Test",
19.27 ["sqroot-test","univariate","equation","test"],
19.28 ["Test","squ-equ-test-subpbl1"]))];
19.29 Iterator 1;
20.1 --- a/test/Tools/isac/Interpret/solve.sml Mon Oct 11 12:55:40 2010 +0200
20.2 +++ b/test/Tools/isac/Interpret/solve.sml Mon Oct 11 13:31:22 2010 +0200
20.3 @@ -42,7 +42,7 @@
20.4 "--------- interSteps on norm_Rational ---------------------------";
20.5 states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
20.6 CalcTree [(["TERM ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
20.7 - ("Rational.thy",
20.8 + ("Rational",
20.9 ["rational","simplification"],
20.10 ["simplification","of_rationals"]))];
20.11 moveActiveRoot 1;
20.12 @@ -145,7 +145,7 @@
20.13 val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
20.14 "realTestFind s"];
20.15 val (dI',pI',mI') =
20.16 - ("Test.thy",["detail","test"],["Test","test_detail_binom"]);
20.17 + ("Test",["detail","test"],["Test","test_detail_binom"]);
20.18
20.19 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.20 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.21 @@ -154,7 +154,7 @@
20.22 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.23 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.25 -(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
20.26 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
20.27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.30 @@ -177,7 +177,7 @@
20.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.32 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.34 - (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
20.35 + (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
20.36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.37 (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
20.38 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
20.39 @@ -208,7 +208,7 @@
20.40 (*15.10.02*)
20.41 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.42 (*
20.43 -rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
20.44 +rewrite "Rationals" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
20.45 "3 ^^^ 2 - x ^^^ 2";
20.46 *)
20.47 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.48 @@ -230,7 +230,7 @@
20.49 val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",
20.50 "realTestFind s"];
20.51 val (dI',pI',mI') =
20.52 - ("Test.thy",["detail","test"],["Test","test_detail_poly"]);
20.53 + ("Test",["detail","test"],["Test","test_detail_poly"]);
20.54
20.55 (*val p = e_pos'; val c = [];
20.56 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
20.57 @@ -242,7 +242,7 @@
20.58 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.59 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.60 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.61 -(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
20.62 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
20.63 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.64 "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
20.65
20.66 @@ -288,7 +288,7 @@
20.67 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.68 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.69 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.70 - (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)
20.71 + (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
20.72 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.73 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
20.74 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
20.75 @@ -357,7 +357,7 @@
20.76 val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
20.77 "realTestFind s"];
20.78 val (dI',pI',mI') =
20.79 - ("Test.thy",["detail","test"],["Test","test_detail_poly"]);
20.80 + ("Test",["detail","test"],["Test","test_detail_poly"]);
20.81
20.82 (* val p = e_pos'; val c = [];
20.83 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
20.84 @@ -369,7 +369,7 @@
20.85 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.86 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.87 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.88 - (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)
20.89 + (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
20.90 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.91 (*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
20.92 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
20.93 @@ -388,7 +388,7 @@
20.94 states:=[];
20.95 CalcTree
20.96 [(["equality (x+1=2)", "solveFor x","solutions L"],
20.97 - ("Test.thy",
20.98 + ("Test",
20.99 ["sqroot-test","univariate","equation","test"],
20.100 ["Test","squ-equ-test-subpbl1"]))];
20.101 Iterator 1;
20.102 @@ -430,7 +430,7 @@
20.103 states:=[];
20.104 CalcTree
20.105 [(["equality (x+1=2)", "solveFor x","solutions L"],
20.106 - ("Test.thy",
20.107 + ("Test",
20.108 ["sqroot-test","univariate","equation","test"],
20.109 ["Test","squ-equ-test-subpbl1"]))];
20.110 Iterator 1;
20.111 @@ -482,7 +482,7 @@
20.112 states:=[];
20.113 CalcTree
20.114 [(["equality (x+1=2)", "solveFor x","solutions L"],
20.115 - ("Test.thy",
20.116 + ("Test",
20.117 ["sqroot-test","univariate","equation","test"],
20.118 ["Test","squ-equ-test-subpbl1"]))];
20.119 Iterator 1;
20.120 @@ -507,7 +507,7 @@
20.121 states:=[];
20.122 CalcTree (*start of calculation, return No.1*)
20.123 [(["equality (x+1=2)", "solveFor x","solutions L"],
20.124 - ("Test.thy",
20.125 + ("Test",
20.126 ["sqroot-test","univariate","equation","test"],
20.127 ["Test","squ-equ-test-subpbl1"]))];
20.128 Iterator 1; moveActiveRoot 1;
21.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml Mon Oct 11 12:55:40 2010 +0200
21.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml Mon Oct 11 13:31:22 2010 +0200
21.3 @@ -14,7 +14,7 @@
21.4 states:=[];
21.5 CalcTree
21.6 [(["equality (x+1=2)", "solveFor x","solutions L"],
21.7 - ("Test.thy",
21.8 + ("Test",
21.9 ["sqroot-test","univariate","equation","test"],
21.10 ["Test","squ-equ-test-subpbl1"]))];
21.11 Iterator 1;
22.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Oct 11 12:55:40 2010 +0200
22.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Mon Oct 11 13:31:22 2010 +0200
22.3 @@ -40,7 +40,7 @@
22.4 " _________________ equation with x =(-12)/5, but L ={} ------- ";
22.5 (* ------------------------------------- *)
22.6 " _________________ rewrite _________________ ";
22.7 -val thy' = "Test.thy";
22.8 +val thy' = "Test";
22.9 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
22.10 val thm = ("square_equation_left","");
22.11 val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
22.12 @@ -213,7 +213,7 @@
22.13 atomty ((#prop o rep_thm) (!tthm));
22.14 atomty (term_of (!tct));
22.15 *)
22.16 -val thy' = "Test.thy";
22.17 +val thy' = "Test";
22.18 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
22.19 (*1*)val thm = ("square_equation_left","");
22.20 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
22.21 @@ -257,7 +257,7 @@
22.22 " _________________ rewrite + cappend _________________ ";
22.23 " _________________ rewrite + cappend _________________ ";
22.24 " _________________ rewrite + cappend _________________ ";
22.25 -val thy' = "Test.thy";
22.26 +val thy' = "Test";
22.27 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
22.28 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
22.29 val oris = prep_ori ctl thy
22.30 @@ -400,8 +400,8 @@
22.31 "solutions L"(*,
22.32 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
22.33 val (dI',pI',mI') =
22.34 - ("Test.thy",["sqroot-test","univariate","equation","test"],
22.35 - ("Test.thy","sqrt-equ-test"));
22.36 + ("Test",["sqroot-test","univariate","equation","test"],
22.37 + ("Test","sqrt-equ-test"));
22.38 val p = e_pos'; val c = [];
22.39 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
22.40
22.41 @@ -414,15 +414,15 @@
22.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.43 (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
22.44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.45 -(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl.thy");
22.46 +(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
22.47 > get_obj g_spec pt (fst p);
22.48 val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
22.49 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.50 (*val nxt = ("Specify_Problem", Specify_Problem *)
22.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.52 -(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*)
22.53 +(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)
22.54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.55 -(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*)
22.56 +(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)
22.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.58 val nxt = ("Free_Solve",Free_Solve);
22.59 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.60 @@ -488,9 +488,9 @@
22.61 val ((p,p_),_,f,nxt,_,pt)=
22.62 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
22.63 (* 5.4.00.: ---
22.64 -get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt;
22.65 +get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;
22.66 val (p,_,f,nxt,_,pt)=
22.67 -me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt;
22.68 +me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
22.69 --- *)
22.70 writeln (pr_ptree pr_short pt);
22.71 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
22.72 @@ -504,7 +504,7 @@
22.73 "solveFor x","errorBound (eps=0)",
22.74 "solutions L"];
22.75 val (dI',pI',mI') =
22.76 - ("Test.thy",["sqroot-test","univariate","equation","test"],
22.77 + ("Test",["sqroot-test","univariate","equation","test"],
22.78 ["Test","sqrt-equ-test"]);
22.79 "--- s1 ---";
22.80 (*val p = e_pos'; val c = [];
22.81 @@ -529,7 +529,7 @@
22.82 val nxt = ("Add_Find",Add_Find "solutions L");
22.83 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.84 "--- s6 ---";
22.85 -val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
22.86 +val nxt = ("Specify_Theory",Specify_Theory "Test");
22.87 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.88 "--- s7 ---";
22.89 val nxt = ("Specify_Problem",
23.1 --- a/test/Tools/isac/OLDTESTS/script.sml Mon Oct 11 12:55:40 2010 +0200
23.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Mon Oct 11 13:31:22 2010 +0200
23.3 @@ -186,7 +186,7 @@
23.4 "--------------------- Notlocatable: Free_Solve ---------------------";
23.5 val fmz = [];
23.6 val (dI',pI',mI') =
23.7 - ("Test.thy",["sqroot-test","univariate","equation","test"],
23.8 + ("Test",["sqroot-test","univariate","equation","test"],
23.9 ["Test","sqrt-equ-test"]);
23.10 (*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
23.11 val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)
23.12 @@ -205,7 +205,7 @@
23.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
23.14 val nxt = ("Add_Find",Add_Find "solutions v_i_");
23.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
23.16 -val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
23.17 +val nxt = ("Specify_Theory",Specify_Theory "Test");
23.18 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
23.19 val nxt =
23.20 ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);
23.21 @@ -256,12 +256,12 @@
23.22 \ (Try (Repeat (Rewrite radd_0 False)))))\
23.23 \ e_e ");
23.24 atomty sc;
23.25 -val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
23.26 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
23.27 ["Test","sqrt-equ-test"]);
23.28 val p = e_pos'; val c = [];
23.29 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
23.30 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
23.31 -val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
23.32 +val nxt = ("Specify_Theory",Specify_Theory "Test");
23.33 val (p,_,_,_,_,pt) = me nxt p c pt;
23.34 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
23.35 val (p,_,_,_,_,pt) = me nxt p c pt;
23.36 @@ -306,7 +306,7 @@
23.37 states:=[];
23.38 CalcTree
23.39 [(["equality (x+1=2)", "solveFor x","solutions L"],
23.40 - ("Test.thy",
23.41 + ("Test",
23.42 ["sqroot-test","univariate","equation","test"],
23.43 ["Test","squ-equ-test-subpbl1"]))];
23.44 Iterator 1;
23.45 @@ -321,7 +321,7 @@
23.46
23.47 val tacs = sel_rules pt ([1],Res);
23.48 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
23.49 - Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
23.50 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
23.51 Check_elementwise "Assumptions"] then ()
23.52 else error "script.sml: diff.behav. in sel_rules ([1],Res)";
23.53
23.54 @@ -336,7 +336,7 @@
23.55
23.56 val tacs = sel_rules pt ([3],Res);
23.57 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
23.58 - Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
23.59 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
23.60 Check_elementwise "Assumptions"] then ()
23.61 else error "script.sml: diff.behav. in sel_rules ([3],Res)";
23.62
24.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Mon Oct 11 12:55:40 2010 +0200
24.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Mon Oct 11 13:31:22 2010 +0200
24.3 @@ -48,7 +48,7 @@
24.4
24.5 rewrite_set "Isac" true
24.6 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
24.7 -rewrite_set "Test.thy" true
24.8 +rewrite_set "Test" true
24.9 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
24.10
24.11
24.12 @@ -63,7 +63,7 @@
24.13 ],
24.14 append_rls e_rls [Calc ("Test.is'_rootequation'_in",
24.15 eval_is_rootequation_in "")],
24.16 - [("Test.thy","methode")]));
24.17 + [("Test","methode")]));
24.18
24.19 match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root'","univariate","equation","test"]);
24.20
24.21 @@ -122,7 +122,7 @@
24.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.25 -(*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)
24.26 +(*val nxt = ("Apply_Method",Apply_Method ("RatArith","solve_linear"))*)
24.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
24.29 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Oct 11 12:55:40 2010 +0200
25.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Oct 11 13:31:22 2010 +0200
25.3 @@ -48,7 +48,7 @@
25.4 \ (Repeat (Rewrite radd_0 False))) g_"
25.5 ));
25.6 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];
25.7 -val (dI',pI',mI') = ("Test.thy",["met_testterm","tests"],
25.8 +val (dI',pI',mI') = ("Test",["met_testterm","tests"],
25.9 ["Test","met_testterm"]);
25.10 (*val p = e_pos'; val c = [];
25.11 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
25.12 @@ -60,7 +60,7 @@
25.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.16 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met_testterm"))*)
25.17 +(*val nxt = ("Apply_Method",Apply_Method ("Test","met_testterm"))*)
25.18 (*----script 111 ------------------------------------------------*)
25.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.20 (*"(#0 + #0) * (#1 * (#1 * a))" nxt= Rewrite ("rmult_1",*)
25.21 @@ -121,7 +121,7 @@
25.22
25.23 val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",
25.24 "boolTestFind v_i_"];
25.25 -val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],
25.26 +val (dI',pI',mI') = ("Test",["met_testeq","tests"],
25.27 ["Test","testeq1"]);
25.28 val Script sc = (#scr o get_met) ["Test","testeq1"];
25.29 atomt sc;
25.30 @@ -135,7 +135,7 @@
25.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.34 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)
25.35 +(*val nxt = ("Apply_Method",Apply_Method ("Test","testeq1")) *)
25.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.38 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.39 @@ -180,7 +180,7 @@
25.40 writeln(term2str sc);
25.41 val fmz = ["boolTestGiven (sqrt a = 0)",
25.42 "boolTestFind v_i_"];
25.43 -val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],
25.44 +val (dI',pI',mI') = ("Test",["met_testeq","tests"],
25.45 ["Test","testlet"]);
25.46 (*val p = e_pos'; val c = [];
25.47 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
25.48 @@ -192,7 +192,7 @@
25.49 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.52 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)
25.53 +(*val nxt = ("Apply_Method",Apply_Method ("Test","testlet"))*)
25.54 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.56 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
25.57 @@ -209,7 +209,7 @@
25.58 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
25.59 "solveFor x","solutions L"];
25.60 val (dI',pI',mI') =
25.61 - ("Test.thy",["sqroot-test","univariate","equation","test"],
25.62 + ("Test",["sqroot-test","univariate","equation","test"],
25.63 ["Test","sqrt-equ-test"]);
25.64 val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
25.65 writeln(term2str sc);
25.66 @@ -234,7 +234,7 @@
25.67 (* val nxt = ("Add_Find",Add_Find "solutions L");*)
25.68 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.69 "--- s6 ---";
25.70 -(* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)
25.71 +(* val nxt = ("Specify_Theory",Specify_Theory "Test");*)
25.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.73 "--- s7 ---";
25.74 (* val nxt =
25.75 @@ -242,10 +242,10 @@
25.76 Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
25.77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.78 "--- s8 ---";
25.79 -(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
25.80 +(* val nxt = ("Specify_Method",Specify_Method ("Test","sqrt-equ-test"));*)
25.81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.82 "--- s9 ---";
25.83 -(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
25.84 +(* val nxt = ("Apply_Method",Apply_Method ("Test","sqrt-equ-test"));*)
25.85 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.86 "--- 1 ---";
25.87 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
25.88 @@ -287,7 +287,7 @@
25.89 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
25.90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.91 "--- 14<> ---";
25.92 -(* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)
25.93 +(* nxt = ("Check_Postcond",Check_Postcond ("Test","sqrt-equ-test"));*)
25.94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.95 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
25.96 then error "scriptnew.sml 1: me + tacs from script: new behaviour"
25.97 @@ -313,7 +313,7 @@
25.98 "solveFor x","errorBound (eps=0)",
25.99 "solutions L"];
25.100 val (dI',pI',mI') =
25.101 - ("Test.thy",["sqroot-test","univariate","equation","test"],
25.102 + ("Test",["sqroot-test","univariate","equation","test"],
25.103 ["Test","sqrt-equ-test"]);
25.104 val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
25.105 (writeln o term2str) sc;
25.106 @@ -337,17 +337,17 @@
25.107 (* val nxt = ("Add_Find",Add_Find "solutions L");*)
25.108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.109 "--- s6 ---";
25.110 -(* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)
25.111 +(* val nxt = ("Specify_Theory",Specify_Theory "Test");*)
25.112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.113 "--- s7 ---";
25.114 (* val nxt = ("Specify_Problem",
25.115 Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
25.116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.117 "--- s8 ---";
25.118 -(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
25.119 +(* val nxt = ("Specify_Method",Specify_Method ("Test","sqrt-equ-test"));*)
25.120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.121 "--- s9 ---";
25.122 -(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
25.123 +(* val nxt = ("Apply_Method",Apply_Method ("Test","sqrt-equ-test"));*)
25.124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
25.125 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"*)
25.126 "--- !!! x1 --- 1.norm_equation";
25.127 @@ -387,7 +387,7 @@
25.128 "solveFor x","errorBound (eps=0)",
25.129 "solutions L"];
25.130 val (dI',pI',mI') =
25.131 - ("Test.thy",["sqroot-test","univariate","equation","test"],
25.132 + ("Test",["sqroot-test","univariate","equation","test"],
25.133 ["Test","square_equation"]);
25.134
25.135 (*val p = e_pos'; val c = [];
25.136 @@ -430,7 +430,7 @@
25.137 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.138 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.139 val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.140 -(*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*)
25.141 +(*val nxt = Subproblem ("Test",["linear","univariate","equation","test"*)
25.142 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.143 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
25.144 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Mon Oct 11 12:55:40 2010 +0200
26.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Mon Oct 11 13:31:22 2010 +0200
26.3 @@ -25,7 +25,7 @@
26.4 val fmz = ["equality (x+1=2)",
26.5 "solveFor x","solutions L"];
26.6 val (dI',pI',mI') =
26.7 - ("Test.thy",["sqroot-test","univariate","equation","test"],
26.8 + ("Test",["sqroot-test","univariate","equation","test"],
26.9 ["Test","squ-equ-test-subpbl1"]);
26.10
26.11 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
26.12 @@ -37,13 +37,13 @@
26.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.14 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
26.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.16 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
26.17 +(*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
26.18 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.19 (*("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation"]*)
26.20 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.21 -(*("Specify_Method",Specify_Method ("Test.thy","squ-equ-test-subpbl1"))*)
26.22 +(*("Specify_Method",Specify_Method ("Test","squ-equ-test-subpbl1"))*)
26.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.24 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","squ-equ-test-subpbl1"*)
26.25 +(*val nxt = ("Apply_Method",Apply_Method ("Test","squ-equ-test-subpbl1"*)
26.26 (*---vvv--- nxt_ here = loc_ below ------------------vvv-------------------*)
26.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.28 (*val f = "x + 1 = 2"; val nxt = Rewrite_Set "norm_equation"*)
26.29 @@ -70,7 +70,7 @@
26.30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.31
26.32
26.33 -(*val f = "-1 + x = 0"; val nxt = Subproblem ("Test.thy",[#,#,#])
26.34 +(*val f = "-1 + x = 0"; val nxt = Subproblem ("Test",[#,#,#])
26.35 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
26.36 (*### locate_gen-----------: is= ### next_tac-----------------: E=
26.37 ScrState (["
26.38 @@ -108,15 +108,15 @@
26.39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.40 (*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * tac*)
26.41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.42 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
26.43 +(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
26.44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.45 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
26.46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.47 -(*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
26.48 +(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
26.49 val Script sc = (#scr o get_met) ["Test","solve_linear"];
26.50 (writeln o term2str) sc;
26.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.52 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
26.53 +(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
26.54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.55 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
26.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.57 @@ -143,7 +143,7 @@
26.58 val fmz = ["equality (1+-1*2+x=0)",
26.59 "solveFor x","solutions L"];
26.60 val (dI',pI',mI') =
26.61 - ("Test.thy",["linear","univariate","equation","test"],
26.62 + ("Test",["linear","univariate","equation","test"],
26.63 ["Test","solve_linear"]);
26.64
26.65 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.66 @@ -154,13 +154,13 @@
26.67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.68 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
26.69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.70 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
26.71 +(*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
26.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.73 (*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
26.74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.75 -(*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
26.76 +(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
26.77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.78 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
26.79 +(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
26.80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.81 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
26.82 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
26.83 @@ -186,7 +186,7 @@
26.84 val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
26.85 "solutions L"];
26.86 val (dI',pI',mI') =
26.87 - ("Test.thy",["plain_square","univariate","equation","test"],
26.88 + ("Test",["plain_square","univariate","equation","test"],
26.89 ["Test","solve_plain_square"]);
26.90 (*val p = e_pos'; val c = [];
26.91 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
26.92 @@ -221,7 +221,7 @@
26.93 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
26.94 "solveFor x","solutions L"];
26.95 val (dI',pI',mI') =
26.96 - ("Test.thy",["sqroot-test","univariate","equation","test"],
26.97 + ("Test",["sqroot-test","univariate","equation","test"],
26.98 ["Test","square_equation1"]);
26.99 (*val p = e_pos'; val c = [];
26.100 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
26.101 @@ -258,7 +258,7 @@
26.102 (*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
26.103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.104 (*"-4 + x = 0"
26.105 - val nxt =("Subproblem",Subproblem ("Test.thy",["linear","univariate"...*)
26.106 + val nxt =("Subproblem",Subproblem ("Test",["linear","univariate"...*)
26.107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.108 (*val nxt =("Model_Problem",Model_Problem ["linear","univariate"...*)
26.109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.110 @@ -266,7 +266,7 @@
26.111
26.112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.114 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
26.115 +(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
26.116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.117 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
26.118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.119 @@ -293,7 +293,7 @@
26.120 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
26.121 "solveFor x","solutions L"];
26.122 val (dI',pI',mI') =
26.123 - ("Test.thy",["sqroot-test","univariate","equation","test"],
26.124 + ("Test",["sqroot-test","univariate","equation","test"],
26.125 ["Test","square_equation2"]);
26.126 val Script sc = (#scr o get_met) ["Test","square_equation2"];
26.127 (writeln o term2str) sc;
26.128 @@ -309,7 +309,7 @@
26.129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.132 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
26.133 +(*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)
26.134 val (p,_,f,nxt,_,pt) =
26.135
26.136 me nxt p [1] pt;
26.137 @@ -322,18 +322,18 @@
26.138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.140 (*"9 + -1 * x ^^^ 2 = 0"
26.141 - Subproblem ("Test.thy",["plain_square","univariate","equation"]))*)
26.142 + Subproblem ("Test",["plain_square","univariate","equation"]))*)
26.143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.144 (*Model_Problem ["plain_square","univariate","equation"]*)
26.145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.149 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
26.150 +(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
26.151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.154 -(*Apply_Method ("Test.thy","solve_plain_square")*)
26.155 +(*Apply_Method ("Test","solve_plain_square")*)
26.156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.157 (*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
26.158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.159 @@ -376,7 +376,7 @@
26.160 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
26.161 "solveFor x","solutions L"];
26.162 val (dI',pI',mI') =
26.163 - ("Test.thy",["squareroot","univariate","equation","test"],
26.164 + ("Test",["squareroot","univariate","equation","test"],
26.165 ["Test","square_equation"]);
26.166 (*val p = e_pos'; val c = [];
26.167 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
26.168 @@ -401,19 +401,19 @@
26.169 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.172 -(*"-4 + x = 0", nxt Subproblem ("Test.thy",["univariate","equation"]))*)
26.173 +(*"-4 + x = 0", nxt Subproblem ("Test",["univariate","equation"]))*)
26.174 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.175 (*val nxt =("Model_Problem",Model_Problem ["linear","univar...*)
26.176 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.178 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.180 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
26.181 +(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
26.182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.183 (*val nxt = ("Specify_Problem",Specify_Problem ["linear","univariate","equ*)
26.184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.186 -(*Apply_Method ("Test.thy","norm_univar_equation")*)
26.187 +(*Apply_Method ("Test","norm_univar_equation")*)
26.188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.191 @@ -436,7 +436,7 @@
26.192 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
26.193 "solveFor x","solutions L"];
26.194 val (dI',pI',mI') =
26.195 - ("Test.thy",["squareroot","univariate","equation","test"],
26.196 + ("Test",["squareroot","univariate","equation","test"],
26.197 ["Test","square_equation"]);
26.198 val Script sc = (#scr o get_met) ["Test","square_equation"];
26.199 (writeln o term2str) sc;
26.200 @@ -452,7 +452,7 @@
26.201 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.204 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
26.205 +(*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)
26.206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.209 @@ -462,14 +462,14 @@
26.210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.213 -(*Subproblem ("Test.thy",["univariate","equation"]))*)
26.214 +(*Subproblem ("Test",["univariate","equation"]))*)
26.215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.216 (*Model_Problem ["plain_square","univariate","equation"]*)
26.217 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.218 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.219 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.221 -(*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
26.222 +(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
26.223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.224 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.225 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.226 @@ -495,7 +495,7 @@
26.227 val fmz = ["equality (1+2*x+3=4*x- 6)",
26.228 "solveFor x","solutions L"];
26.229 val (dI',pI',mI') =
26.230 - ("Test.thy",["univariate","equation","test"],
26.231 + ("Test",["univariate","equation","test"],
26.232 ["no_met"]);
26.233 (*val p = e_pos'; val c = [];
26.234 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
26.235 @@ -509,11 +509,11 @@
26.236 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.237 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.238 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.239 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","norm_univar_equation"*)
26.240 +(*val nxt = ("Apply_Method",Apply_Method ("Test","norm_univar_equation"*)
26.241 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.242 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.243 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.244 -(*val nxt = ("Subproblem",Subproblem ("Test.thy",["univariate","equation"])*)
26.245 +(*val nxt = ("Subproblem",Subproblem ("Test",["univariate","equation"])*)
26.246 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.247 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
26.248 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.249 @@ -523,7 +523,7 @@
26.250 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.251 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.252 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.253 -(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
26.254 +(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
26.255 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.256 val (p,_,f,nxt,_,pt) = me nxt p c pt;
26.257 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Mon Oct 11 12:55:40 2010 +0200
27.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Mon Oct 11 13:31:22 2010 +0200
27.3 @@ -14,7 +14,7 @@
27.4 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
27.5 states:=[];
27.6 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
27.7 - ("Test.thy",
27.8 + ("Test",
27.9 ["sqroot-test","univariate","equation","test"],
27.10 ["Test","squ-equ-test-subpbl1"]))];
27.11 Iterator 1; moveActiveRoot 1;
27.12 @@ -85,7 +85,7 @@
27.13 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
27.14 states:=[];
27.15 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
27.16 - ("Test.thy",
27.17 + ("Test",
27.18 ["sqroot-test","univariate","equation","test"],
27.19 ["Test","squ-equ-test-subpbl1"]))];
27.20 Iterator 1; moveActiveRoot 1;
27.21 @@ -104,7 +104,7 @@
27.22 val str = pr_ptree pr_short pt;
27.23 writeln str;
27.24
27.25 - setNextTactic 1 (Subproblem ("Test.thy",["linear","univariate",
27.26 + setNextTactic 1 (Subproblem ("Test",["linear","univariate",
27.27 "equation","test"]));
27.28 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*);
27.29 val ((pt,_),_) = get_calc 1;
28.1 --- a/test/Tools/isac/ProgLang/listg.sml Mon Oct 11 12:55:40 2010 +0200
28.2 +++ b/test/Tools/isac/ProgLang/listg.sml Mon Oct 11 13:31:22 2010 +0200
28.3 @@ -45,7 +45,7 @@
28.4 "--------------------- length_ -------------------------------------------";
28.5 "--------------------- length_ -------------------------------------------";
28.6 "--------------------- length_ -------------------------------------------";
28.7 -val thy' = "ListG.thy";
28.8 +val thy' = "ListG";
28.9 val ct = "length_ [1,1,1]";
28.10 val thm = ("length_Cons_","");
28.11 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
29.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Mon Oct 11 12:55:40 2010 +0200
29.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Mon Oct 11 13:31:22 2010 +0200
29.3 @@ -60,7 +60,7 @@
29.4 CalcTree
29.5 [(["TERM (b + a - b)",(*this is Schalk 299b*)
29.6 "normalform N"],
29.7 - ("Poly.thy",["polynomial","simplification"],
29.8 + ("Poly",["polynomial","simplification"],
29.9 ["Test","test_interSteps_1"]))];
29.10 Iterator 1;
29.11 moveActiveRoot 1;
29.12 @@ -96,7 +96,7 @@
29.13 states:=[];
29.14 CalcTree
29.15 [(["TERM (b + a - b)", "normalform N"],
29.16 - ("Poly.thy",["polynomial","simplification"],
29.17 + ("Poly",["polynomial","simplification"],
29.18 ["simplification","for_polynomials"]))];
29.19 Iterator 1;
29.20 moveActiveRoot 1;
29.21 @@ -155,7 +155,7 @@
29.22 states:=[];
29.23 CalcTree
29.24 [(["TERM (b + a - b)", "normalform N"],
29.25 - ("Poly.thy",["polynomial","simplification"],
29.26 + ("Poly",["polynomial","simplification"],
29.27 ["simplification","of_rationals"]))];
29.28 Iterator 1;
29.29 moveActiveRoot 1;
30.1 --- a/test/Tools/isac/Test_Isac.thy Mon Oct 11 12:55:40 2010 +0200
30.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Oct 11 13:31:22 2010 +0200
30.3 @@ -118,7 +118,7 @@
30.4 (* TODO
30.5 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
30.6
30.7 -*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
30.8 +*** Could not find theory file "Foo_Language" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
30.9 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
30.10
30.11 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
31.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Oct 11 12:55:40 2010 +0200
31.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Oct 11 13:31:22 2010 +0200
31.3 @@ -76,7 +76,7 @@
31.4 collect_rlss ("IsacKnowledge",thy');
31.5
31.6 "collect_thy thy-------------------------------------------------";
31.7 -val thy' = "ListG.thy";
31.8 +val thy' = "ListG";
31.9 val thy = assoc_thy (thyID2theory' thy');
31.10 ((collect_thms' ("IsacKnowledge",thy')) @
31.11 (collect_rlss ("IsacKnowledge",thy')) @
31.12 @@ -151,7 +151,7 @@
31.13
31.14 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
31.15 see sml/../datatypes.sml !
31.16 -val (thy', rls') = ("DiffApp.thy", "Tools.rhs");
31.17 +val (thy', rls') = ("DiffApp", "Tools.rhs");
31.18 thy_containing_rls thy' rls';
31.19 print_depth 99; map #1 startsearch; print_depth 3;
31.20 *)