# HG changeset patch # User Walther Neuper # Date 1283957242 -7200 # Node ID 02844267398126df08fa492cacb7b85db656f601 # Parent 24609758d219575e92d2307c0ad934c50498c6ef tuned src + test find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \; find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \; find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \; find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \; find . -type f -exec sed -i s/" L_"/" L_L"/g {} \; find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \; find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \; find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \; find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \; diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Diff.thy --- a/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:47:22 2010 +0200 @@ -283,26 +283,26 @@ prls=e_rls, crls = Atools_erls, nrls = norm_diff}, "Script DiffScr (f_::real) (v_v::real) = " ^ " (let f'_ = Take (d_d v_v f_) " ^ -" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^ +" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ " (Repeat " ^ -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^ +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)" +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)" )); store_met @@ -317,22 +317,22 @@ " (let f'_ = Take (d_d v_v f_) " ^ " in (( " ^ " (Repeat " ^ -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^ +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ " (Repeat (Rewrite_Set make_polynomial False)))) " ^ " )) f'_)" )); @@ -347,27 +347,27 @@ srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff}, "Script DiffEqScr (f_::bool) (v_v::real) = " ^ " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) " ^ -" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^ +" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ " (Repeat " ^ -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^ -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^ +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)" +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)" )); store_met @@ -381,9 +381,9 @@ "Script DiffScr (f_::real) (v_v::real) = " ^ " (let f'_ = Take (d_d v_v f_) " ^ " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ " ^ -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^ +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ +" (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^ +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^ " (Try (Rewrite_Set norm_Rational False))) f'_)" )); @@ -404,7 +404,7 @@ castab := overwritel (!castab, [((term_of o the o (parse thy)) "Diff", - (("Isac.thy", ["derivative_of","function"], ["no_met"]), + (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss)) ]); @@ -422,7 +422,7 @@ castab := overwritel (!castab, [((term_of o the o (parse thy)) "Differentiate", - (("Isac.thy", ["named","derivative_of","function"], ["no_met"]), + (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss)) ]); *} diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/DiffApp-oldscr.sml --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 16:47:22 2010 +0200 @@ -22,7 +22,7 @@ ML> set show_types; ML> c; val c = - "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_::real set err_::bool = + "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool = let e_e::bool = (hd o filter (Testvar m_)) rs_; t_::real = if (#1::real) < Length rs_ diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/DiffApp-scrpbl.sml --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Sep 08 16:47:22 2010 +0200 @@ -315,7 +315,7 @@ "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"]; val (dI',pI',mI')= - ("DiffAppl.thy",["Script.thy","maximum_of","function"],e_metID); + ("DiffAppl",["Script","maximum_of","function"],e_metID); val c = []:cid; (* @@ -416,7 +416,7 @@ "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]", "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]; val (dI',pI',mI')= - ("DiffAppl.thy",["DiffAppl.thy","test_maximum"],e_metID); + ("DiffAppl",["DiffAppl","test_maximum"],e_metID); val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI'))); diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/DiffApp.sml --- a/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 16:47:22 2010 +0200 @@ -3,17 +3,17 @@ *) -theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]); +theory' := overwritel (!theory', [("DiffAppl",DiffAppl.thy)]); (* -> get_pbt ["DiffAppl.thy","maximum_of","function"]; -> get_met ("Script.thy","max_on_interval_by_calculus"); +> get_pbt ["DiffAppl","maximum_of","function"]; +> get_met ("Script","max_on_interval_by_calculus"); > !pbltypes; *) pbltypes:= overwritel (!pbltypes, [ prep_pbt DiffAppl.thy - (["DiffAppl.thy","maximum_of","function"], + (["DiffAppl","maximum_of","function"], [("#Given" ,"fixedValues fix_"), ("#Find" ,"maximum m_"), ("#Find" ,"valuesFor vs_"), @@ -25,7 +25,7 @@ ]), prep_pbt DiffAppl.thy - (["DiffAppl.thy","make","function"]:pblID, + (["DiffAppl","make","function"]:pblID, [("#Given" ,"functionOf f_"), ("#Given" ,"boundVariable v_v"), ("#Given" ,"equalities eqs_"), @@ -33,7 +33,7 @@ ]), prep_pbt DiffAppl.thy - (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID, + (["DiffAppl","on_interval","maximum_of","function"]:pblID, [("#Given" ,"functionTerm t_"), ("#Given" ,"boundVariable v_v"), ("#Given" ,"interval itv_"), @@ -41,7 +41,7 @@ ]), prep_pbt DiffAppl.thy - (["DiffAppl.thy","find_values","tool"]:pblID, + (["DiffAppl","find_values","tool"]:pblID, [("#Given" ,"maxArgument ma_"), ("#Given" ,"functionTerm f_"), ("#Given" ,"boundVariable v_v"), @@ -53,7 +53,7 @@ methods:= overwritel (!methods, [ - (("DiffAppl.thy","max_by_calculus"):metID, + (("DiffAppl","max_by_calculus"):metID, {ppc = prep_met DiffAppl.thy [("#Given" ,"fixedValues fix_"), ("#Given" ,"boundVariable v_v"), @@ -66,7 +66,7 @@ rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], scr=EmptyScr} : met), - (("DiffAppl.thy","make_fun_by_new_variable"):metID, + (("DiffAppl","make_fun_by_new_variable"):metID, {ppc = prep_met DiffAppl.thy [("#Given" ,"functionOf f_"), ("#Given" ,"boundVariable v_v"), @@ -76,7 +76,7 @@ rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], scr=EmptyScr} : met), - (("DiffAppl.thy","make_fun_by_explicit"):metID, + (("DiffAppl","make_fun_by_explicit"):metID, {ppc = prep_met DiffAppl.thy [("#Given" ,"functionOf f_"), ("#Given" ,"boundVariable v_v"), @@ -86,7 +86,7 @@ rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], scr=EmptyScr} : met), - (("DiffAppl.thy","max_on_interval_by_calculus"):metID, + (("DiffAppl","max_on_interval_by_calculus"):metID, {ppc = prep_met DiffAppl.thy [("#Given" ,"functionTerm t_"), ("#Given" ,"boundVariable v_v"), @@ -97,7 +97,7 @@ rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], scr=EmptyScr} : met), - (("DiffAppl.thy","find_values"):metID, + (("DiffAppl","find_values"):metID, {ppc = prep_met DiffAppl.thy [], rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/DiffApp.thy --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 16:47:22 2010 +0200 @@ -162,7 +162,7 @@ crls = eval_rls, nrls=norm_Rational (*, asm_rls=[],asm_thm=[]*)}, "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^ - " (v_v::real) (itv_::real set) (err_::bool) = " ^ + " (v_v::real) (itv_v::real set) (err_::bool) = " ^ " (let e_e = (hd o (filterVar m_)) rs_; " ^ " t_ = (if 1 < length_ rs_ " ^ " then (SubProblem (DiffApp_,[make,function],[no_met]) " ^ diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 16:47:22 2010 +0200 @@ -137,10 +137,10 @@ val (f, ts) = strip_comb t and (g, us) = strip_comb u; val _=writeln("t= f@ts= \""^ ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ - (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\""); + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\""); val _=writeln("u= g@us= \""^ ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ - (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\""); + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\""); val _=writeln("size_of_term(t,u)= ("^ (string_of_int(size_of_term' t))^", "^ (string_of_int(size_of_term' u))^")"); @@ -158,10 +158,10 @@ end | ord => ord) and hd_ord (f, g) = (* ~ term.ML *) - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) and terms_ord str pr (ts, us) = - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); (**) in (**) @@ -260,7 +260,7 @@ erls = Atools_erls, srls = Erls, calc = [], rules = [Thm ("left_distrib",num_str @{thm left_distrib}), (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) - Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}), + Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}), (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) Rls_ norm_Rational_noadd_fractions(**2**), diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Equation.thy --- a/src/Tools/isac/Knowledge/Equation.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Sep 08 16:47:22 2010 +0200 @@ -78,10 +78,10 @@ castab := overwritel (!castab, [((term_of o the o (parse thy)) "solveTest", - (("Test.thy", ["univariate","equation","test"], ["no_met"]), + (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)), ((term_of o the o (parse thy)) "solve", - (("Isac.thy", ["univariate","equation"], ["no_met"]), + (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss)) ]); diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/InsSort.sml --- a/src/Tools/isac/Knowledge/InsSort.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/InsSort.sml Wed Sep 08 16:47:22 2010 +0200 @@ -20,7 +20,7 @@ (*-------------------------from InsSort.ML 8.3.01----------------------*) -theory' := (!theory') @ [("InsSort.thy",InsSort.thy)]; +theory' := (!theory') @ [("InsSort",InsSort.thy)]; val ins_sort = Rls{preconds = [], rew_ord = ("tless_true",tless_true), @@ -42,13 +42,13 @@ (* -> get_pbt ["Script.thy","squareroot","univariate","equation"]; -> get_met ("Script.thy","max_on_interval_by_calculus"); +> get_pbt ["Script","squareroot","univariate","equation"]; +> get_met ("Script","max_on_interval_by_calculus"); *) pbltypes:= (!pbltypes) @ [ prep_pbt InsSort.thy - (["InsSort.thy","inssort"]:pblID, + (["InsSort","inssort"]:pblID, [("#Given" ,"unsorted u_"), ("#Find" ,"sorted s_") ]) @@ -57,13 +57,13 @@ methods:= (!methods) @ [ (*, -------17.6.00, - (("InsSort.thy","inssort"):metID, + (("InsSort","inssort"):metID, {ppc = prep_met [("#Given" ,"unsorted u_"), ("#Find" ,"sorted s_") ], rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], - scr=Script (((inst_abs (assoc_thm "InsSort.thy")) + scr=Script (((inst_abs (assoc_thm "InsSort")) o term_of o the o (parse thy)) (*for [#1,#3,#2] only*) "Script Ins_sort (u_::'a list) = \ \ (let u_ = Rewrite sort_def False u_; \ @@ -85,7 +85,7 @@ \ in u_)") } : met), - (("InsSort.thy","sort"):metID, + (("InsSort","sort"):metID, {ppc = prep_met [("#Given" ,"unsorted u_"), ("#Find" ,"sorted s_") diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Integrate.thy --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 16:47:22 2010 +0200 @@ -241,8 +241,8 @@ (*"?bdv / ?b = (1 / ?b) * ?bdv"*) Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) - *****Thm ("nadd_divide_distrib", - *****num_str @{thm nadd_divide_distrib}) + *****Thm ("add_divide_distrib", + *****num_str @{thm add_divide_distrib}) (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) ]; val simplify_Integral = @@ -252,7 +252,7 @@ calc = [], (*asm_thm = [],*) rules = [Thm ("left_distrib",num_str @{thm left_distrib}), (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) - Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}), + Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}), (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) Rls_ norm_Rational_noadd_fractions, @@ -294,8 +294,8 @@ * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) * Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) -* Thm ("nadd_divide_distrib", -* num_str @{thm nadd_divide_distrib}) +* Thm ("add_divide_distrib", +* num_str @{thm add_divide_distrib}) * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) * ]), * Calc ("HOL.divide" ,eval_cancel "#divide_e") @@ -369,7 +369,7 @@ crls = Atools_erls, nrls = e_rls}, "Script IntegrationScript (f_::real) (v_v::real) = " ^ " (let t_ = Take (Integral f_ D v_v) " ^ -" in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))" +" in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))" )); store_met @@ -384,8 +384,8 @@ crls = Atools_erls, nrls = e_rls}, "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^ " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^ -" in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@ " ^ -" (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_) " +" in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ +" (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) " )); *} diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/LogExp.thy --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 08 16:47:22 2010 +0200 @@ -32,10 +32,10 @@ (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID (["logarithmic","univariate","equation"], [("#Given",["equality e_e","solveFor v_v"]), - ("#Where",["matches ((?a log ?v_) = ?b) e_e"]), + ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), ("#Find" ,["solutions v_i"]), - ("#With" ,["||(lhs (Subst (v_i_,v_) e_e) - " ^ - " (rhs (Subst (v_i_,v_) e_e) || < eps)"]) + ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^ + " (rhs (Subst (v_i_,v_v) e_e) || < eps)"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]])); @@ -45,7 +45,7 @@ (prep_met thy "met_equ_log" [] e_metID (["Equation","solve_log"], [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Where" ,["matches ((?a log ?v_) = ?b) e_e"]), + ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), ("#Find" ,["solutions v_i"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Poly.thy --- a/src/Tools/isac/Knowledge/Poly.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Sep 08 16:47:22 2010 +0200 @@ -475,7 +475,7 @@ and hd_ord (f, g) = (* ~ term.ML *) prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) and terms_ord str pr (ts, us) = - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); in fun ord_make_polynomial (pr:bool) thy (_:subst) tu = diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 16:47:22 2010 +0200 @@ -1102,7 +1102,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* @@ -1129,7 +1129,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* @@ -1156,7 +1156,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* @@ -1180,7 +1180,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* @@ -1204,7 +1204,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* @@ -1228,7 +1228,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* @@ -1258,7 +1258,7 @@ " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions} )" + " in Check_elementwise L_LL {(v_v::real). Assumptions} )" )); *} ML{* diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/RatEq.thy --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Sep 08 16:47:22 2010 +0200 @@ -214,7 +214,7 @@ " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^ " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^ " [BOOL e_e, REAL v_v]) " ^ - " in Check_elementwise L_L {(v_v::real). Assumptions})" + " in Check_elementwise L_LL {(v_v::real). Assumptions})" )); *} diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Root.thy --- a/src/Tools/isac/Knowledge/Root.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Sep 08 16:47:22 2010 +0200 @@ -140,7 +140,7 @@ prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) and terms_ord str pr (ts, us) = - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); in (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 08 16:47:22 2010 +0200 @@ -575,7 +575,7 @@ " [no_met]) [BOOL e_e, REAL v_v]) " ^ " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^ " [BOOL e_e, REAL v_v])) " ^ -"in Check_elementwise L_L {(v_v::real). Assumptions})" +"in Check_elementwise L_LL {(v_v::real). Assumptions})" )); *} diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Test.sml --- a/src/Tools/isac/Knowledge/Test.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.sml Wed Sep 08 16:47:22 2010 +0200 @@ -1,7 +1,7 @@ val ttt = (term_of o the o (parse thy)) -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e"; +"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e"; val ttt = (term_of o the o (parse thy)) -"(Try (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) e_e)"; +"(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)"; val ttt = (term_of o the o (parse thy)) "(Rewrite_Set SqRoot_simplify False) e_e "; @@ -32,7 +32,7 @@ val ttt = (term_of o the o (parse thy)) "Script Solve_linear (e_e::bool) (v_v::real)= \ \(let e_e = \ - \ (Repeat ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False)) e_e)\ + \ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\ \ in [e_])"; (*----*) val ttt = (term_of o the o (parse thy)) @@ -42,7 +42,7 @@ "Script Solve_linear (e_e::bool) (v_v::real)= \ \(let e_e = \ \ (Repeat\ - \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\ + \ ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\ \ e_e)\ \ e_e)\ \ in [e_])"; @@ -51,7 +51,7 @@ \(let e_e = \ \ (Repeat\ \ ((%ee_.\ - \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_))\ + \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\ \ e_e)\ \ e_e)\ \ in [e_])"; @@ -60,7 +60,7 @@ \(let e_e = \ \ (Repeat\ \ ((%ee_.\ - \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) ee_)\ + \ (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\ \ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\ \ e_e)\ \ e_e)\ @@ -121,22 +121,22 @@ "Script Solve_linear (e_e::bool) (v_v::real)= \ \(let e_e = \ \ ((Repeat\ - \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ + \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ \ (Rewrite_Set SqRoot_simplify False)))) e_e)\ \ in [e_])"; atomty ttt; val ttt = (term_of o the o (parse thy)) -"(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@ yyy"; +"(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy"; atomty ttt; val ttt = (term_of o the o (parse thy)) - "(Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ + "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ \ (Rewrite_Set SqRoot_simplify False)"; atomty ttt; val ttt = (term_of o the o (parse thy)) "(Repeat\ - \ ((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ + \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ \ (Rewrite_Set SqRoot_simplify False))) e_e"; atomty ttt; val ttt = (term_of o the o (parseold thy)) @@ -150,7 +150,7 @@ "Script Solve_linear (e_e::bool) (v_v::real)= \ \(let e_e =\ \ Repeat\ - \ (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@\ + \ (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\ \ (Rewrite_Set SqRoot_simplify False))) e_\ \ in [e_::bool])" ; diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 16:47:22 2010 +0200 @@ -597,7 +597,7 @@ "Script Solve_linear (e_e::bool) (v_v::real)= " ^ "(let e_e =" ^ " Repeat" ^ - " (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^ + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ " (Rewrite_Set Test_simplify False))) e_e" ^ " in [e_::bool])" ) @@ -897,7 +897,7 @@ " (Try (Rewrite_Set Test_simplify False)))) @@" ^ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)) @@" ^ - " (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^ + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ " e_e" ^ " in [e_::bool])" @@ -927,12 +927,12 @@ " (Try (Rewrite_Set Test_simplify False)))) @@" ^ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)) @@" ^ - " (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^ + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ - " e_;" ^ + " e_e;" ^ " (L_::bool list) = Tac subproblem_equation_dummy; " ^ - " L_ = Tac solve_equation_dummy " ^ - " in Check_elementwise L_ {(v_v::real). Assumptions})" + " L_L = Tac solve_equation_dummy " ^ + " in Check_elementwise L_L {(v_v::real). Assumptions})" )); store_met @@ -946,10 +946,10 @@ crls=tval_rls, nrls=Test_simplify}, "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^ - " (Try (Rewrite_Set Test_simplify False))) e_; " ^ + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^ "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^ " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^ - "in Check_elementwise L_ {(v_v::real). Assumptions})" + "in Check_elementwise L_L {(v_v::real). Assumptions})" )); store_met @@ -964,10 +964,10 @@ asm_rls=[],asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)}, "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^ - " (let e_e = Try (Rewrite_Set norm_equation False) e_; " ^ + " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^ "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^ " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^ - "in Check_elementwise L_ {(v_v::real). Assumptions})" + "in Check_elementwise L_L {(v_v::real). Assumptions})" )); store_met @@ -994,11 +994,11 @@ " (Try (Rewrite_Set Test_simplify False)))) @@" ^ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ - " e_;" ^ + " e_e;" ^ " (L_::bool list) = " ^ " (SubProblem (Test_,[linear,univariate,equation,test]," ^ " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^ - "in Check_elementwise L_ {(v_v::real). Assumptions})" + "in Check_elementwise L_L {(v_v::real). Assumptions})" )); store_met @@ -1025,10 +1025,10 @@ " (Try (Rewrite_Set Test_simplify False)))) @@" ^ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ - " e_;" ^ + " e_e;" ^ " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^ " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^ - " in Check_elementwise L_ {(v_v::real). Assumptions})" + " in Check_elementwise L_L {(v_v::real). Assumptions})" )); store_met @@ -1056,10 +1056,10 @@ " (Try (Rewrite_Set Test_simplify False)))) @@" ^ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ - " e_;" ^ + " e_e;" ^ " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^ " [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^ - " in Check_elementwise L_ {(v_v::real). Assumptions})" + " in Check_elementwise L_L {(v_v::real). Assumptions})" )); store_met @@ -1087,10 +1087,10 @@ " (Try (Rewrite_Set Test_simplify False)))) @@" ^ " (Try (Rewrite_Set norm_equation False)) @@" ^ " (Try (Rewrite_Set Test_simplify False)))" ^ - " e_;" ^ + " e_e;" ^ " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^ " [no_met]) [BOOL e_e, REAL v_])" ^ - " in Check_elementwise L_ {(v_v::real). Assumptions})" + " in Check_elementwise L_L {(v_v::real). Assumptions})" ) ); (*#######*) store_met @@ -1200,9 +1200,9 @@ end | ord => ord) and hd_ord (f, g) = (* ~ term.ML *) - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) and terms_ord str pr (ts, us) = - list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); + list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); in fun ord_make_polytest (pr:bool) thy (_:subst) tu = diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/algein.sml --- a/test/Tools/isac/Knowledge/algein.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Sep 08 16:47:22 2010 +0200 @@ -64,7 +64,7 @@ "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]", "GesamtLaenge L"]; val (dI',pI',mI') = - ("Isac.thy",["numerischSymbolische", "Berechnung"], + ("Isac",["numerischSymbolische", "Berechnung"], ["Berechnung","erstNumerisch"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*); @@ -77,7 +77,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*); -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin.thy"*); +val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*); @@ -108,7 +108,7 @@ "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]", "GesamtLaenge L"], - ("Isac.thy",["numerischSymbolische", "Berechnung"], + ("Isac",["numerischSymbolische", "Berechnung"], ["Berechnung","erstSymbolisch"]))]; Iterator 1; moveActiveRoot 1; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/biegelinie.sml --- a/test/Tools/isac/Knowledge/biegelinie.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Sep 08 16:47:22 2010 +0200 @@ -54,7 +54,7 @@ "----------- Script [IntegrierenUndKonstanteBestimmen] -----------"; val str = "Script BiegelinieScript \ -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \ +\(l_::real) (q__::real) (v_v::real) (b_::real=>real) \ \(rb_::bool list) (rm_::bool list) = \ \ (let q___ = Take (q_ v_v = q__); \ \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \ @@ -181,7 +181,7 @@ "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"]; val (dI',pI',mI') = - ("Biegelinie.thy",["MomentBestimmte","Biegelinien"], + ("Biegelinie",["MomentBestimmte","Biegelinien"], ["IntegrierenUndKonstanteBestimmen"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -213,7 +213,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; case nxt of - (_,Subproblem ("Biegelinie.thy", ["named", "integrate", "function"])) => () + (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => () | _ => raise error "biegelinie.sml: Bsp 7.27 #4c"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -231,7 +231,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; case nxt of - (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>() + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>() | _ => raise error "biegelinie.sml: Bsp 7.27 #5b"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -259,7 +259,7 @@ if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then () else raise error "biegelinie.sml: Bsp 7.27 #9"; -(*val nxt = (+, Subproblem ("Biegelinie.thy", ["normalize", ..lin..sys]))*) +(*val nxt = (+, Subproblem ("Biegelinie", ["normalize", ..lin..sys]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -299,7 +299,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; case nxt of - (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>() + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>() | _ => raise error "biegelinie.sml: Bsp 7.27 #13"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -321,7 +321,7 @@ "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)" then () else raise error "biegelinie.sml: Bsp 7.27 #16 f"; case nxt of - (_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>() + (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>() | _ => raise error "biegelinie.sml: Bsp 7.27 #16"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -349,7 +349,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; case nxt of (_, Subproblem - ("Biegelinie.thy", ["normalize", "2x2", "linear", "system"])) => () + ("Biegelinie", ["normalize", "2x2", "linear", "system"])) => () | _ => raise error "biegelinie.sml: Bsp 7.27 #19"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -367,7 +367,7 @@ else raise error "biegelinie.sml: Bsp 7.27 #21 f"; case nxt of (_, Subproblem - ("Biegelinie.thy", ["triangular", "2x2", "linear", "system"])) =>() + ("Biegelinie", ["triangular", "2x2", "linear", "system"])) =>() | _ => raise error "biegelinie.sml: Bsp 7.27 #21"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -454,7 +454,7 @@ "RandbedingungenBiegung [y 0 = 0, y L = 0]", "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", + ("Biegelinie", ["MomentBestimmte","Biegelinien"], ["IntegrierenUndKonstanteBestimmen"]))]; moveActiveRoot 1; @@ -500,7 +500,7 @@ \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\ \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\ \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"]; -val (dI',pI',mI') = ("Biegelinie.thy", ["vonBelastungZu","Biegelinien"], +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"], ["Biegelinien","ausBelastung"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -618,7 +618,7 @@ val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)", "substitution (M_b L = 0)", "equality equ___"]; -val (dI',pI',mI') = ("Biegelinie.thy", ["makeFunctionTo","equation"], +val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"], ["Equation","fromFunction"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -764,7 +764,7 @@ \y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]", "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", "Gleichungen equs___"]; -val (dI',pI',mI') = ("Biegelinie.thy", ["setzeRandbedingungen","Biegelinien"], +val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"], ["Biegelinien","setzeRandbedingungenEin"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -920,7 +920,7 @@ "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------"; "----- script "; val str = -"Script Belastung2BiegelScript (q__::real) (v_::real) = \ +"Script Belastung2BiegelScript (q__::real) (v_v::real) = \ \ (let q___ = Take (q_ v_v = q__); \ \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \ \ (Rewrite Belastung_Querkraft True)) q___; \ @@ -954,7 +954,7 @@ val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"]; -val (dI',pI',mI') = ("Biegelinie.thy", ["Biegelinien"], +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -975,7 +975,7 @@ #b# prep_met ... (["Biegelinien","ausBelastung"], ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), - "Script Belastung2BiegelScript (q__::real) (v_::real) = \ + "Script Belastung2BiegelScript (q__::real) (v_v::real) = \ #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK ########################################################################## @@ -989,7 +989,7 @@ CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["Biegelinien"], + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 16:47:22 2010 +0200 @@ -86,7 +86,7 @@ "----------- for correction of diff_const ------------------------"; "----------- for correction of diff_const ------------------------"; (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*) -val thy' = "Diff.thy"; +val thy' = "Diff"; val ct = "Not (x =!= a)"; rewrite_set thy' false "erls" ct; val ct = "2 is_const"; @@ -127,7 +127,7 @@ " _________________ for correction of diff_quot _________________ "; " _________________ for correction of diff_quot _________________ "; " _________________ for correction of diff_quot _________________ "; -val thy' = "Diff.thy"; +val thy' = "Diff"; val ct = "Not (x = 0)"; rewrite_set thy' false "erls" ct; @@ -145,7 +145,7 @@ " _________________ differentiate by rewrite _________________ "; " _________________ differentiate by rewrite _________________ "; " _________________ differentiate by rewrite _________________ "; -val thy' = "Diff.thy"; +val thy' = "Diff"; val ct = "d_d x (x ^^^ 2 + 3 * x + 4)"; "--- 1 ---"; val thm = ("diff_sum",""); @@ -197,7 +197,7 @@ val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", "differentiateFor x","derivative f_'_"]; val (dI',pI',mI') = - ("Diff.thy",["derivative_of","function"], + ("Diff",["derivative_of","function"], ["diff","diff_simpl"]); val p = e_pos'; val c = []; "--- s1 ---"; @@ -258,7 +258,7 @@ trace_rewrite:=false; val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0"; - val SOME (ct',_) = rewrite_set "Isac.thy" false "make_polynomial" ct; + val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct; trace_rewrite:=true; val t = str2term ct; @@ -274,7 +274,7 @@ case string_of_thm thm of - val Rewrite_Set' ("Diff.thy",false,"make_polynomial",ff,(ff',[])) = m; + val Rewrite_Set' ("Diff",false,"make_polynomial",ff,(ff',[])) = m; term2str ff; term2str ff'; @@ -285,7 +285,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; "--- 8 ---"; (*val nxt = -("Check_Postcond",Check_Postcond ("Diff.thy","differentiate_on_R"));*) +("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*) val (p,_,f,nxt,_,pt) = me nxt p c pt; "--- 9 ---"; (*val nxt = ("End_Proof'",End_Proof');*) @@ -303,35 +303,35 @@ " _________________ script-eval corrected _________________ "; " _________________ script-eval corrected _________________ "; " _________________ script-eval corrected _________________ "; -val scr = Script (((inst_abs (assoc_thy "Test.thy")) o +val scr = Script (((inst_abs (assoc_thy "Test")) o term_of o the o (parse Diff.thy)) - "Script Differentiate (f_::real) (v_::real) = \ + "Script Differentiate (f_::real) (v_v::real) = \ \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \ \ f_ = Try (Repeat (Rewrite root_conv False f_)); \ \ f_ = Repeat \ - \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False f_)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False f_)) Or \ + \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False f_)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False f_)) Or \ \ (Repeat (Rewrite_Set Test_simplify False f_))); \ \ f_ = Try (Repeat (Rewrite sym_frac_conv False f_)) \ \ in Try (Repeat (Rewrite sym_root_conv False f_)))"); val d = e_rls; val (dI',pI',mI') = - ("Diff.thy",e_pblID, - ("Diff.thy","differentiate_on_R")); + ("Diff",e_pblID, + ("Diff","differentiate_on_R")); val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; @@ -352,45 +352,45 @@ val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete; val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum",""))); -val NextStep(l1,m') = nxt_tac "Diff.thy" (pt,p) scr ets0 l0; +val NextStep(l1,m') = nxt_tac "Diff" (pt,p) scr ets0 l0; (*("diff_sum","")*) val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets0 l0; + locate_gen "Diff" m' (pt,p) (scr,d) ets0 l0; val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; " --------------- 2. ---------------------------------------------"; val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum",""))); -val NextStep(l2,m') = nxt_tac "Diff.thy" (pt,p) scr ets1 l1; +val NextStep(l2,m') = nxt_tac "Diff" (pt,p) scr ets1 l1; (*("diff_sum","")*) val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets1 l1; + locate_gen "Diff" m' (pt,p) (scr,d) ets1 l1; val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; " --------------- 3. ---------------------------------------------"; val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const",""))); -val NextStep(l3,m') = nxt_tac "Diff.thy" (pt,p) scr ets2 l2; +val NextStep(l3,m') = nxt_tac "Diff" (pt,p) scr ets2 l2; (*("diff_prod_const","")*) val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets2 l2; + locate_gen "Diff" m' (pt,p) (scr,d) ets2 l2; val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; " --------------- 4. ---------------------------------------------"; val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow",""))); -val NextStep(l4,m') = nxt_tac "Diff.thy" (pt,p) scr ets3 l3; +val NextStep(l4,m') = nxt_tac "Diff" (pt,p) scr ets3 l3; (*("diff_pow","")*) val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets3 l3; + locate_gen "Diff" m' (pt,p) (scr,d) ets3 l3; val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; " --------------- 5. ---------------------------------------------"; val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const",""))); -val NextStep(l5,m') = nxt_tac "Diff.thy" (pt,p) scr ets4 l4; +val NextStep(l5,m') = nxt_tac "Diff" (pt,p) scr ets4 l4; (*("diff_const","")*) val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] = - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets4 l4; + locate_gen "Diff" m' (pt,p) (scr,d) ets4 l4; val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)]; " --------------- 6. ---------------------------------------------"; val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var",""))); -val NextStep(l6,m') = nxt_tac "Diff.thy" (pt,p) scr ets5 l5; +val NextStep(l6,m') = nxt_tac "Diff" (pt,p) scr ets5 l5; (*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*) val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] = - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets5 l5; + locate_gen "Diff" m' (pt,p) (scr,d) ets5 l5; val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)]; " --------------- 7. ---------------------------------------------"; val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify"); @@ -412,7 +412,7 @@ val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", "differentiateFor x","derivative f_'_"]; val (dI',pI',mI') = - ("Diff.thy",["derivative_of","function"], + ("Diff",["derivative_of","function"], ["diff","differentiate_on_R"]); *) @@ -427,7 +427,7 @@ val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", "differentiateFor x","derivative f_'_"]; val (dI',pI',mI') = - ("Diff.thy",["derivative_of","function"], + ("Diff",["derivative_of","function"], ["diff","differentiate_on_R"]); *) @@ -439,7 +439,7 @@ val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", "differentiateFor x","derivative f_'_"]; val (dI',pI',mI') = - ("Diff.thy",["derivative_of","function"], + ("Diff",["derivative_of","function"], ["diff","diff_simpl"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -452,7 +452,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*nxt = ("Apply_Method",Apply_Method ("Diff.thy","differentiate_on_R*) +(*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -486,30 +486,30 @@ else raise error "diff.sml: diff.behav. in 'primed'"; atomty f'_; -val str = "Script DiffEqScr (f_::bool) (v_::real) = \ +val str = "Script DiffEqScr (f_::bool) (v_v::real) = \ \ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \ \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \ \ (Try (Repeat (Rewrite root_conv False))) @@ \ \ (Try (Repeat (Rewrite realpow_pow False))) @@ \ \ (Repeat \ - \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \ - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \ + \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or \ + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \ \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \ \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \ \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)" @@ -568,7 +568,7 @@ [(["functionTerm (x^2 + x+ 1/x + 2/x^2)", (*"functionTerm ((x^3)^5)",*) "differentiateFor x", "derivative f_'_"], - ("Isac.thy", ["derivative_of","function"], + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; Iterator 1; moveActiveRoot 1; @@ -583,7 +583,7 @@ CalcTree [(["functionTerm (x^3 * x^5)", "differentiateFor x", "derivative f_'_"], - ("Isac.thy", ["derivative_of","function"], + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; Iterator 1; moveActiveRoot 1; @@ -608,7 +608,7 @@ CalcTree [(["functionTerm (x^3 * x^5)", "differentiateFor x", "derivative f_'_"], - ("Isac.thy", ["derivative_of","function"], + ("Isac", ["derivative_of","function"], ["diff","after_simplification"]))]; Iterator 1; moveActiveRoot 1; @@ -628,7 +628,7 @@ CalcTree [(["functionTerm ((x^3)^5)", "differentiateFor x", "derivative f_'_"], - ("Isac.thy", ["derivative_of","function"], + ("Isac", ["derivative_of","function"], ["diff","after_simplification"]))]; Iterator 1; moveActiveRoot 1; @@ -645,7 +645,7 @@ states:=[]; CalcTree [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"], - ("Isac.thy", ["named","derivative_of","function"], + ("Isac", ["named","derivative_of","function"], ["diff","differentiate_equality"]))]; Iterator 1; moveActiveRoot 1; @@ -677,7 +677,7 @@ CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"], - ("Isac.thy", ["derivative_of","function"], + ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; Iterator 1; moveActiveRoot 1; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 16:47:22 2010 +0200 @@ -129,7 +129,7 @@ (* --vvv-- ausgeliehen von test-root-equ/sml *) val loc = e_istate; val (dI',pI',mI') = - ("Script.thy",["sqroot-test","univariate","equation"], + ("Script",["sqroot-test","univariate","equation"], ["Script","squ-equ-test2"]); val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", "solveFor x","errorBound (eps=0)", @@ -266,7 +266,7 @@ "interval {x::real. 0 <= x & x <= pi}", "errorBound (eps=(0::real))"]; val (dI',pI',mI') = - ("DiffApp.thy",["maximum_of","function"], + ("DiffApp",["maximum_of","function"], ["DiffApp","max_by_calculus"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -295,7 +295,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; (*since 0508 Apply_Method does the 1st step, if NONE init_form ------------- -(*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*) +(*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*) val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e; (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -339,7 +339,7 @@ # presumerably didnt work before either, but not detected due to Emtpy_Tac # ############################################################################ -(*val nxt = Subproblem ("DiffApp.thy",["univariate","equation"])) *) +(*val nxt = Subproblem ("DiffApp",["univariate","equation"])) *) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Refine_Tacitly ["univariate","equation"])*) @@ -407,7 +407,7 @@ "interval {x::real. 0 <= x & x <= pi}", "errorBound (eps=(0::real))"]; val (dI',pI',mI') = - ("DiffApp.thy",["maximum_of","function"], + ("DiffApp",["maximum_of","function"], ["DiffApp","max_by_calculus"]); CalcTree [(fmz, (dI',pI',mI'))]; @@ -444,7 +444,7 @@ "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; str2term "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ - \ (v_::real) (itv_::real set) (err_::bool) = \ + \ (v_v::real) (itv_v::real set) (err_::bool) = \ \ (let e_e = (hd o (filterVar m_)) rs_; \ \ t_ = (if 1 < length_ rs_ \ \ then (SubProblem (Reals_,[make,function],[no_met])\ @@ -463,9 +463,9 @@ str2term "A"); val rs_ = (str2term "rs_::bool list", str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"); -val v_v = (str2term "v_::real", +val v_v = (str2term "v_v::real", str2term "b"); -val itv_ = (str2term "itv_::real set", +val itv_ = (str2term "itv_v::real set", str2term "{x::real. 0 <= x & x <= 2*r}"); val err_ = (str2term "err_::bool", str2term "eps=0"); @@ -519,7 +519,7 @@ "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; str2term - "Script Make_fun_by_explicit (f_::real) (v_::real) \ + "Script Make_fun_by_explicit (f_::real) (v_v::real) \ \ (eqs_::bool list) = \ \ (let h_ = (hd o (filterVar f_)) eqs_; \ \ e_1 = hd (dropWhile (ident h_) eqs_); \ @@ -530,7 +530,7 @@ \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; val f_ = (str2term "f_::real", str2term "A"); -val v_v = (str2term "v_::real", +val v_v = (str2term "v_v::real", str2term "b"); val eqs_=(str2term "eqs_::bool list", str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"); @@ -610,7 +610,7 @@ "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; str2term - "Script Make_fun_by_new_variable (f_::real) (v_::real) \ + "Script Make_fun_by_new_variable (f_::real) (v_v::real) \ \ (eqs_::bool list) = \ \(let h_ = (hd o (filterVar f_)) eqs_; \ \ es_ = dropWhile (ident h_) eqs_; \ @@ -626,7 +626,7 @@ \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; val f_ = (str2term "f_::real", str2term "A"); -val v_v = (str2term "v_::real", +val v_v = (str2term "v_v::real", str2term "alpha"); val eqs_=(str2term "eqs_::bool list", str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"); diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/eqsystem.sml --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 16:47:22 2010 +0200 @@ -865,7 +865,7 @@ \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]", "solveForVars [c, c_2]", "solution L"]; val (dI',pI',mI') = - ("Biegelinie.thy",["normalize", "2x2", "linear", "system"], + ("Biegelinie",["normalize", "2x2", "linear", "system"], ["EqSystem","normalize","2x2"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -883,7 +883,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; case nxt of - (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => () + (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => () | _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -933,7 +933,7 @@ \ -1 * q_0 / 24 * L ^^^ 4)]", "solveForVars [c, c_2]", "solution L"]; val (dI',pI',mI') = - ("Biegelinie.thy",["linear", "system"], ["no_met"]); + ("Biegelinie",["linear", "system"], ["no_met"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -952,7 +952,7 @@ "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]" then () else raise error "eqsystem.sml me simpl. before SubProblem b"; case nxt of - (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => () + (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => () | _ => raise error "eqsystem.sml me [linear,system] SubProblem b"; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1004,7 +1004,7 @@ CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["Biegelinien"], + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]; moveActiveRoot 1; (* @@ -1045,7 +1045,7 @@ "Biegelinie y", "Randbedingungen [y L = 0, y' L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"], + ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"], ["Biegelinien", "AusMomentenlinie"]))]; moveActiveRoot 1; (* @@ -1057,7 +1057,7 @@ CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["Biegelinien"], + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))]; moveActiveRoot 1; (* @@ -1077,7 +1077,7 @@ CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["Biegelinien"], + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))]; moveActiveRoot 1; (* @@ -1125,7 +1125,7 @@ \ 0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution L"]; val (dI',pI',mI') = - ("Biegelinie.thy",["linear", "system"],["no_met"]); + ("Biegelinie",["linear", "system"],["no_met"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1303,7 +1303,7 @@ \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]", "solveForVars [c, c_2, c_3, c_4]", "solution L"]; val (dI',pI',mI') = - ("Biegelinie.thy",["linear", "system"],["no_met"]); + ("Biegelinie",["linear", "system"],["no_met"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1328,7 +1328,7 @@ CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["Biegelinien"], + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))]; moveActiveRoot 1; (* @@ -1350,7 +1350,7 @@ "Biegelinie y", "Randbedingungen [y 0 = 0, y L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"], + ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"], ["Biegelinien", "AusMomentenlinie"]))]; moveActiveRoot 1; (* @@ -1362,7 +1362,7 @@ CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y", "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["Biegelinien"], + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))]; moveActiveRoot 1; (* @@ -1383,7 +1383,7 @@ "Biegelinie y", "Randbedingungen [y L = 0, y' L = 0]", "FunktionsVariable x"], - ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"], + ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"], ["Biegelinien", "AusMomentenlinie"]))]; moveActiveRoot 1; (* @@ -1403,7 +1403,7 @@ \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]", "solveForVars [c, c_2, c_3, c_4]", "solution L"]; val (dI',pI',mI') = - ("Biegelinie.thy",["normalize", "4x4", "linear", "system"], + ("Biegelinie",["normalize", "4x4", "linear", "system"], ["EqSystem","normalize","4x4"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/inssort.sml --- a/test/Tools/isac/Knowledge/inssort.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/inssort.sml Wed Sep 08 16:47:22 2010 +0200 @@ -6,7 +6,7 @@ WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *) "--------------- sort [1,4,3,2] by rewrite_set ----------------"; -val thy' = "InsSort.thy"; +val thy' = "InsSort"; val ct = "sort [1,4,3,2]"; "--- 1 ---"; val rls = "ins_sort"; @@ -16,7 +16,7 @@ "---------------- sort [1,3,2] by rewrite stepwise ----------------"; -val thy' = "InsSort.thy"; +val thy' = "InsSort"; val ct = "sort [1,3,2]"; "--- 1 ---"; val thm = ("sort_def",""); @@ -89,7 +89,7 @@ "---------------- sort [1,3,2] from script ----------------"; val fmz = ["unsorted [1,3,2]", "sorted S"]; val (dI',pI',mI') = - ("InsSort.thy", ["inssort","functional"], ("InsSort.thy","inssort")); + ("InsSort", ["inssort","functional"], ("InsSort","inssort")); val p = e_pos'; val c = []; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 16:47:22 2010 +0200 @@ -248,7 +248,7 @@ val rls = "integration_rules"; val subs = [("bdv","x::real")]; fun rewrit_sinst subs rls str = - fst (the (rewrite_set_inst "Integrate.thy" true subs rls str)); + fst (the (rewrite_set_inst "Integrate" true subs rls str)); (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) val str = rewrit_sinst subs rls "Integral x D x"; val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x"; @@ -362,16 +362,16 @@ "----------- check Scripts ---------------------------------------"; "----------- check Scripts ---------------------------------------"; val str = -"Script IntegrationScript (f_::real) (v_::real) = \ +"Script IntegrationScript (f_::real) (v_v::real) = \ \ (let t_ = Take (Integral f_ D v_v) \ -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"; +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; atomty sc; val str = -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \ +"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \ \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \ -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"; +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)"; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; atomty sc; show_mets(); @@ -384,7 +384,7 @@ val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x","antiDerivative FF"]; val (dI',pI',mI') = - ("Integrate.thy",["integrate","function"], + ("Integrate",["integrate","function"], ["diff","integration"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -409,7 +409,7 @@ val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x","antiDerivativeName F"]; val (dI',pI',mI') = - ("Integrate.thy",["named","integrate","function"], + ("Integrate",["named","integrate","function"], ["diff","integration","named"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -434,7 +434,7 @@ val fmz = ["functionTerm (- q_0)", "integrateBy x","antiDerivativeName Q"]; val (dI',pI',mI') = - ("Biegelinie.thy",["named","integrate","function"], + ("Biegelinie",["named","integrate","function"], ["diff","integration","named"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -460,7 +460,7 @@ states:=[]; CalcTree [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], - ("Integrate.thy",["integrate","function"], + ("Integrate",["integrate","function"], ["diff","integration"]))]; Iterator 1; moveActiveRoot 1; @@ -486,17 +486,17 @@ srls = e_rls, prls=e_rls, crls = Atools_erls, nrls = e_rls}, -"Script IntegrationScript (f_::real) (v_::real) = \ -\ (((Rewrite_Set_Inst [(bdv,v_)] integration_rules False) @@ \ -\ (Rewrite_Set_Inst [(bdv,v_)] add_new_c False) @@ \ -\ (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) (f_::real))" +"Script IntegrationScript (f_::real) (v_v::real) = \ +\ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \ +\ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \ +\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))" )); states:=[]; CalcTree [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x", "antiDerivative FF"], - ("Integrate.thy",["integrate","function"], + ("Integrate",["integrate","function"], ["diff","integration","test"]))]; Iterator 1; moveActiveRoot 1; @@ -527,7 +527,7 @@ states:=[]; CalcTree [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], - ("Integrate.thy",["integrate","function"], + ("Integrate",["integrate","function"], ["diff","integration"]))]; Iterator 1; moveActiveRoot 1; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/logexp.sml --- a/test/Tools/isac/Knowledge/logexp.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed Sep 08 16:47:22 2010 +0200 @@ -36,7 +36,7 @@ val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"]; val (dI',pI',mI') = - ("Isac.thy",["logarithmic","univariate","equation","test"], + ("Isac",["logarithmic","univariate","equation","test"], ["Test","solve_log"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Sep 08 16:47:22 2010 +0200 @@ -395,7 +395,7 @@ \- (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"]; val (dI',pI',mI') = - ("Poly.thy",["polynomial","simplification"], + ("Poly",["polynomial","simplification"], ["simplification","for_polynomials"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -420,7 +420,7 @@ states:=[]; CalcTree [(["TERM ((x - y)*(x + y))", "normalform N"], - ("Poly.thy",["polynomial","simplification"], + ("Poly",["polynomial","simplification"], ["simplification","for_polynomials"]))]; Iterator 1; moveActiveRoot 1; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/polyeq.sml --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 08 16:47:22 2010 +0200 @@ -125,7 +125,7 @@ "----- d0_false ------"; (*EP*) val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"], ["PolyEq","solve_d0_polyeq_equation"]); (*val p = e_pos'; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -143,7 +143,7 @@ "----- d0_true ------"; (*EP-7*) val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"], ["PolyEq","solve_d0_polyeq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -167,7 +167,7 @@ "----- d2_pqformula1 ------!!!!"; val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -194,7 +194,7 @@ "----- d2_pqformula1_neg ------"; (*EP-8*) val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -217,7 +217,7 @@ "----- d2_pqformula2 ------"; val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -237,7 +237,7 @@ "----- d2_pqformula2_neg ------"; val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -258,7 +258,7 @@ "----- d2_pqformula3 ------"; (*EP-9*) val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -277,7 +277,7 @@ "----- d2_pqformula3_neg ------"; val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -297,7 +297,7 @@ "----- d2_pqformula4 ------"; val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -316,7 +316,7 @@ "----- d2_pqformula4_neg ------"; val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -334,7 +334,7 @@ "----- d2_pqformula5 ------"; val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -353,7 +353,7 @@ "----- d2_pqformula6 ------"; val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -373,7 +373,7 @@ "----- d2_pqformula7 ------"; (*EP-10*) val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -392,7 +392,7 @@ "----- d2_pqformula8 ------"; val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -412,7 +412,7 @@ "----- d2_pqformula9 ------"; val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -432,7 +432,7 @@ "----- d2_pqformula10_neg ------"; val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -452,7 +452,7 @@ "----- d2_pqformula10 ------"; val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -471,7 +471,7 @@ "----- d2_pqformula9_neg ------"; val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -493,7 +493,7 @@ "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -511,7 +511,7 @@ | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]"; val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -530,7 +530,7 @@ (*EP-11*) val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -548,7 +548,7 @@ | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]"; val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -567,7 +567,7 @@ "TODO 1 + x + 2*x^^^2 = 0"; val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -585,7 +585,7 @@ | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]"; val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -605,7 +605,7 @@ (*EP-12*) val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -623,7 +623,7 @@ | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]"; val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -643,7 +643,7 @@ (*EP-13*) val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -661,7 +661,7 @@ | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]"; val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -680,7 +680,7 @@ (*EP-14*) val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -698,7 +698,7 @@ val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -716,7 +716,7 @@ (*EP-15*) val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -734,7 +734,7 @@ | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -753,7 +753,7 @@ (*EP-16*) val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -772,7 +772,7 @@ (*EP-//*) val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -795,7 +795,7 @@ val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*) "solveFor x","solutions L"]; val (dI',pI',mI') = - ("PolyEq.thy",["degree_2","expanded","univariate","equation"], + ("PolyEq",["degree_2","expanded","univariate","equation"], ["PolyEq","complete_square"]); (* val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -806,7 +806,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; - (*Apply_Method ("PolyEq.thy","complete_square")*) + (*Apply_Method ("PolyEq","complete_square")*) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*) val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -854,7 +854,7 @@ val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)", "solveFor x","solutions L"]; val (dI',pI',mI') = - ("PolyEq.thy",["degree_2","expanded","univariate","equation"], + ("PolyEq",["degree_2","expanded","univariate","equation"], ["PolyEq","complete_square"]); (* val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -868,7 +868,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; - (*Apply_Method ("PolyEq.thy","complete_square")*) + (*Apply_Method ("PolyEq","complete_square")*) val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------"; @@ -877,7 +877,7 @@ val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; val (dI',pI',mI') = - ("PolyEq.thy",["degree_2","expanded","univariate","equation"], + ("PolyEq",["degree_2","expanded","univariate","equation"], ["PolyEq","complete_square"]); (* val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -891,7 +891,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; - (*Apply_Method ("PolyEq.thy","complete_square")*) + (*Apply_Method ("PolyEq","complete_square")*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -913,7 +913,7 @@ val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)", "solveFor x","solutions L"]; val (dI',pI',mI') = - ("PolyEq.thy",["degree_2","expanded","univariate","equation"], + ("PolyEq",["degree_2","expanded","univariate","equation"], ["PolyEq","complete_square"]); (* val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -956,7 +956,7 @@ val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*) "solveFor x","solutions L"]; val (dI',pI',mI') = - ("PolyEq.thy",["degree_2","expanded","univariate","equation"], + ("PolyEq",["degree_2","expanded","univariate","equation"], ["PolyEq","complete_square"]); (* val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -987,7 +987,7 @@ val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*) "solveFor x","solutions L"]; val (dI',pI',mI') = - ("PolyEq.thy",["degree_2","expanded","univariate","equation"], + ("PolyEq",["degree_2","expanded","univariate","equation"], ["PolyEq","complete_square"]); (* val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1017,7 +1017,7 @@ val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"]; (* refine fmz ["univariate","equation"]; *) -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1036,7 +1036,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* val nxt = ("Subproblem", - Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) + Subproblem ("PolyEq",["polynomial","univariate","equation"])) : string * tac *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val nxt = @@ -1061,7 +1061,7 @@ (*is in rlang.sml, too*) val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1082,7 +1082,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* val nxt = ("Subproblem", - Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) + Subproblem ("PolyEq",["polynomial","univariate","equation"])) : string * tac*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val nxt = @@ -1106,7 +1106,7 @@ val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"]; (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*) (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*) -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1169,7 +1169,7 @@ states:=[]; CalcTree [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"], - ("PolyEq.thy",["univariate","equation"],["no_met"]))]; + ("PolyEq",["univariate","equation"],["no_met"]))]; Iterator 1; moveActiveRoot 1; autoCalculate 1 CompleteCalc; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 08 16:47:22 2010 +0200 @@ -252,7 +252,7 @@ states:=[]; CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -265,7 +265,7 @@ states:=[]; CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -279,7 +279,7 @@ states:=[]; CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -292,7 +292,7 @@ states:=[]; CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -305,7 +305,7 @@ states:=[]; CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -320,7 +320,7 @@ "----------- met probe fuer_polynom ------------------------------"; val str = "Script ProbeScript (e_e::bool) (ws_::bool list) =\ -\ (let e_e = Take e_; \ +\ (let e_e = Take e_e; \ \ e_e = Substitute ws_ e_e \ \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \ \ (Try (Repeat (Calculate PLUS ))) @@ \ @@ -337,7 +337,7 @@ \3 - 2 * e + 2 * f + 2 * g)", "mitWert [e = 1, f = 2, g = 3]", "Geprueft b"], - ("PolyMinus.thy",["polynom","probe"], + ("PolyMinus",["polynom","probe"], ["probe","fuer_polynom"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -359,7 +359,7 @@ states:=[]; CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))", "normalform N"], - ("PolyMinus.thy",["klammer","polynom","vereinfachen"], + ("PolyMinus",["klammer","polynom","vereinfachen"], ["simplification","for_polynomials","with_parentheses"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -374,7 +374,7 @@ CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)", "mitWert [u = 2]", "Geprueft b"], - ("PolyMinus.thy",["polynom","probe"], + ("PolyMinus",["polynom","probe"], ["probe","fuer_polynom"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -390,7 +390,7 @@ states:=[]; CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalcHead; @@ -450,7 +450,7 @@ states:=[]; CalcTree [(["TERM (- (8 * g) + 10 * g + h)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -462,7 +462,7 @@ states:=[]; CalcTree [(["TERM (- (8 * g) + 10 * g + f)", "normalform N"], - ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], + ("PolyMinus",["plus_minus","polynom","vereinfachen"], ["simplification","for_polynomials","with_minus"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -511,7 +511,7 @@ states:=[]; CalcTree [(["TERM ((3*a + 2) * (4*a - 1))", "normalform N"], - ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"], + ("PolyMinus",["binom_klammer","polynom","vereinfachen"], ["simplification","for_polynomials","with_parentheses_mult"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; @@ -530,7 +530,7 @@ states:=[]; CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"], - ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"], + ("PolyMinus",["binom_klammer","polynom","vereinfachen"], ["simplification","for_polynomials","with_parentheses_mult"]))]; moveActiveRoot 1; autoCalculate 1 CompleteCalc; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Sep 08 16:47:22 2010 +0200 @@ -46,7 +46,7 @@ (* refine fmz ["univariate","equation"]; *) -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt; --------------------------------------- Refine_Tacitly*) @@ -56,7 +56,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])*) +(* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt; --------------------------------------- Refine_Tacitly*) @@ -73,7 +73,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* val nxt = ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +(* val nxt = ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) @@ -104,7 +104,7 @@ (* refine fmz ["univariate","equation"]; *) -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -118,7 +118,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*) +(* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -127,7 +127,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *) +(* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = ("Model_Problem", Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])*) diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/rational-old.sml --- a/test/Tools/isac/Knowledge/rational-old.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/rational-old.sml Wed Sep 08 16:47:22 2010 +0200 @@ -242,7 +242,7 @@ val (t,asm) = the (rewrite_set_ thy eval_rls false rls t); -val thy' = "Rational.thy"; +val thy' = "Rational"; val rls' = "cancel"; val t' = "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)"; val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); @@ -250,12 +250,12 @@ else raise error "tests/rationals.sml(1): new behaviour";*) -val thy' = "Rational.thy"; +val thy' = "Rational"; val rls' = "cancel"; val t' = "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c + 7 * a^^^2 * b * c) "; val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); -val thy' = "Rational.thy"; +val thy' = "Rational"; val rls' = "cancel"; val t' = "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )"; val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); @@ -274,7 +274,7 @@ Schalk Reniets Verlag *) -val thy' = "Rational.thy"; +val thy' = "Rational"; val rls' = "cancel"; val mp = "make_polynomial"; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Sep 08 16:47:22 2010 +0200 @@ -472,7 +472,7 @@ "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------"; "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------"; "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------"; -val thy' = "Rational.thy"; +val thy' = "Rational"; val rls' = "cancel"; val mp = "make_polynomial"; @@ -1828,7 +1828,7 @@ val fmz = ["TERM ((14 * x * y) / ( x * y ))", "normalform N"]; val (dI',pI',mI') = - ("Rational.thy",["rational","simplification"], + ("Rational",["rational","simplification"], ["simplification","of_rationals"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; @@ -1854,7 +1854,7 @@ states:=[]; CalcTree [(["TERM (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"], - ("Rational.thy",["rational","simplification"], + ("Rational",["rational","simplification"], ["simplification","of_rationals"]))]; Iterator 1; moveActiveRoot 1; @@ -1871,7 +1871,7 @@ states:=[]; CalcTree [(["TERM ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"], - ("Rational.thy",["rational","simplification"], + ("Rational",["rational","simplification"], ["simplification","of_rationals"]))]; Iterator 1; moveActiveRoot 1; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/rlang.sml --- a/test/Tools/isac/Knowledge/rlang.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Sep 08 16:47:22 2010 +0200 @@ -57,7 +57,7 @@ (*EP*) val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -88,7 +88,7 @@ (*EP*) val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -118,7 +118,7 @@ (*EP*) val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -148,7 +148,7 @@ (*EP*) val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -178,7 +178,7 @@ (*ER-2*) val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -220,7 +220,7 @@ (*ER-1*) val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -260,7 +260,7 @@ (*ER-3*) val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -300,7 +300,7 @@ (*ER-4*) val fmz = ["equality ((x+3)/(2*x - 4)=3)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -342,7 +342,7 @@ (*ER-5*) val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -388,7 +388,7 @@ (*ER-6*) val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -425,7 +425,7 @@ (*ER-7*) val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*val nxt = ("Model_Problem",Model_Problem["rational","univariate","equation"*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -445,7 +445,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 040209 MGs norm_Rational*) -(* val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*) +(* val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*) if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0"))then() else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b"; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -511,7 +511,7 @@ (*ER-8*) val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -551,7 +551,7 @@ (*ER-10*) val fmz = ["equality (m1*v1+m2*v2=0)", "solveFor m1","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -580,7 +580,7 @@ (*ER-11*) val fmz = ["equality (f=((w+u)/(w+v))*v0)", "solveFor v","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -595,7 +595,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*nxt = Subproblem ("RatEq.thy",["univariate","equation"])) *) +(*nxt = Subproblem ("RatEq",["univariate","equation"])) *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -605,7 +605,7 @@ (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*val nxt =Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +(*val nxt =Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) if f = Form' (FormKF (~1, @@ -659,7 +659,7 @@ (*ER-12*) val fmz = ["equality (f=((w+u)/(w+v))*v0)", "solveFor w","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos';val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -707,7 +707,7 @@ (*ER-9*) val fmz = ["equality (1/R=1/R1+1/R2)", "solveFor R1","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -752,7 +752,7 @@ (*ER-13 + EO-11 ?!?*) val fmz = ["equality (y^^^2=2*p*x)", "solveFor p","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) @@ -785,7 +785,7 @@ (*EO ??*) val fmz = ["equality (y^^^2=2*p*x)", "solveFor y","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -818,7 +818,7 @@ (*EO-8*) val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -868,7 +868,7 @@ (*ER-14*) val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))", "solveFor x2","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -907,7 +907,7 @@ (*EO*) val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -945,7 +945,7 @@ "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)"; val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1028,7 +1028,7 @@ (*EO-2*) val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1039,7 +1039,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x" --> Subproblem ("RootEq.thy", ["univariate", ...])*) +-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1048,7 +1048,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2" --> Subproblem ("RootEq.thy", ["univariate", ...])*) +-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1078,7 +1078,7 @@ (*EO-3*) val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1089,7 +1089,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*4 + 5 * x + -2 * sqrt (3 + 13 * x + 4 * x ^^^ 2) = -2 + x" --> Subproblem ("RootEq.thy", ["univariate", ...])*) +-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1099,7 +1099,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*"12 + 52 * x + 16 * x ^^^ 2 = 36 + x ^^^ 2 + 48 * x + 15 * x ^^^ 2" --> Subproblem ("RootEq.thy", ["univariate", ...])*) +-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1108,7 +1108,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then () else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a"; -(*-> ubproblem ("PolyEq.thy", ["degree_1", ...]*) +(*-> ubproblem ("PolyEq", ["degree_1", ...]*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1130,7 +1130,7 @@ (*EO-4*) val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *) @@ -1193,7 +1193,7 @@ (*EP*) val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1222,7 +1222,7 @@ (*ER-15*) val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1233,7 +1233,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f; (*"(-4 + x) * (1 + x) = (1 + -1 * x) * (4 + x)" --> Subproblem ("RatEq.thy", ["univariate", ...])*) +-> Subproblem ("RatEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1243,7 +1243,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then () else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a"; -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*) +(*-> Subproblem ("PolyEq", ["polynomial", ...])*) (* val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f; *) @@ -1265,7 +1265,7 @@ "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))"; val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1307,7 +1307,7 @@ "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)"; val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1358,7 +1358,7 @@ *) val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1401,7 +1401,7 @@ "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))"; val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))", "solveFor a","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -1446,23 +1446,23 @@ "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)"; val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*val nxt = ("Specify_Theory",Specify_Theory "RatEq.thy")*) +(*val nxt = ("Specify_Theory",Specify_Theory "RatEq")*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val p = ([3],Res) val f="1 * (a * (b * x)) = (a * b + (a * x + -1 * (b * x))) * (b + (x + -1 * a) -val nxt = Subproblem ("RatEq.thy",["univariate","equation"]))*) +val nxt = Subproblem ("RatEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*) +(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = Specify_Problem ["normalize","polynomial","univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1471,7 +1471,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*) (*val p = ([4,5],Res) val f ="b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0")) -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) if f = Form' (FormKF (~1, @@ -1483,7 +1483,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*) +(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*Specify_Problem["abcFormula","degree_2","polynomial","univariate","equation*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1507,7 +1507,7 @@ (*----------------- Schalk II s.68 Bsp 56a ------------------------*) "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))"; val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1595,7 +1595,7 @@ "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))"; val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*) @@ -1657,7 +1657,7 @@ "Schalk II s.68 Bsp 62b (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)"; val fmz = ["equality (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1718,7 +1718,7 @@ (*EO-7*) val fmz = ["equality ((2*x+1)*x^^^2 = 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -1769,7 +1769,7 @@ (*EO-9*) val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)", "solveFor a","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* Model_Problem ["normalize","polynomial","univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1779,7 +1779,7 @@ (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*) +(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt =Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"])*) @@ -1815,7 +1815,7 @@ (*EO-10*) val fmz = ["equality (2*sqrt(r^^^2 - (u/2)^^^2) - u^^^2/(2*sqrt(r^^^2 - (u/2)^^^2))= 0)", "solveFor u","solutions L"]; -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (* Model_Problem ["normalize","root'","univariate","equation"])*) @@ -1825,7 +1825,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Apply_Method ["RootEq","norm_sq_root_equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*) +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1836,7 +1836,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*) +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Model_Problem ["rational","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1846,7 +1846,7 @@ (*val nxt = Apply_Method ["RootEq","solve_rat_equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*) +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Model_Problem ["normalize","polynomial","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -1856,7 +1856,7 @@ (*val nxt = Apply_Method ["PolyEq","normalize_poly"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) if f = Form' (FormKF (~1, diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/rooteq.sml --- a/test/Tools/isac/Knowledge/rooteq.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Sep 08 16:47:22 2010 +0200 @@ -88,7 +88,7 @@ (*---------rooteq---- 23.8.02 ---------------------*) "---------(1/sqrt(x)=5)---------------------"; val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -97,14 +97,14 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*"1 / x = 25" -> Subproblem ("RootEq.thy", ["univariate", ...]) *) +(*"1 / x = 25" -> Subproblem ("RootEq", ["univariate", ...]) *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*"1 = 25 * x" -> Subproblem ("RatEq.thy", ["univariate", ...])*) +(*"1 = 25 * x" -> Subproblem ("RatEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -113,7 +113,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then () else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)"; -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*) +(*-> Subproblem ("PolyEq", ["polynomial", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -137,7 +137,7 @@ "---------(sqrt(x+1)=5)---------------------"; val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -149,7 +149,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -158,7 +158,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then () else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5"; -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*) +(*-> Subproblem ("PolyEq", ["polynomial", ...])*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -173,7 +173,7 @@ "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------"; val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -207,7 +207,7 @@ "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------"; val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *) @@ -219,7 +219,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x")) -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -230,7 +230,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2")) -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -239,7 +239,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then () else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr.."; -(*-> Subproblem ("PolyEq.thy", ["degree_0", ...])*) +(*-> Subproblem ("PolyEq", ["degree_0", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -260,7 +260,7 @@ val fmz = ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"], +val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"], ["RootEq","solve_sq_root_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -274,7 +274,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2")) -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"])) *) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"])) *) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -283,7 +283,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0")) -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then () else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt.."; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -311,7 +311,7 @@ "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----"; val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"], +val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"], ["RootEq","solve_sq_root_equation"]); (*val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); @@ -326,7 +326,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; (* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1")) -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -335,7 +335,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0")) -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then () else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt.."; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -372,7 +372,7 @@ "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\ \ with same error"; val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"], +val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"], ["RootEq","solve_sq_root_equation"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -383,7 +383,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x")) -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -392,7 +392,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0")) -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*) +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*) if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then () else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt.."; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -420,7 +420,7 @@ "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------"; val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -431,7 +431,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; (* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *) val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -442,7 +442,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; (*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2")) -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*) +val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -451,7 +451,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then () else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt.."; -(*-> Subproblem ("PolyEq.thy", ["degree_1", ...])*) +(*-> Subproblem ("PolyEq", ["degree_1", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Sep 08 16:47:22 2010 +0200 @@ -50,7 +50,7 @@ "--------------------- test thm rootrat_equation_left_1 ---------------------"; val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -59,21 +59,21 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -82,7 +82,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then () else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1"; -(*-> Subproblem ("RootEq.thy", ["polynomial", ...])*) +(*-> Subproblem ("RootEq", ["polynomial", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -98,7 +98,7 @@ "--------------------- test thm rootrat_equation_left_2 ---------------------"; val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -106,21 +106,21 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*) +(*-> Subproblem ("RootEq", ["univariate", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -129,7 +129,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then () else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2"; -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*) +(*-> Subproblem ("PolyEq", ["polynomial", ...])*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -145,7 +145,7 @@ "--------------------- test thm rootrat_equation_right_1 ---------------"; val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -188,7 +188,7 @@ "--------------------- test thm rootrat_equation_right_2 --------------------"; val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"]; -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/simplify.sml --- a/test/Tools/isac/Knowledge/simplify.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/simplify.sml Wed Sep 08 16:47:22 2010 +0200 @@ -41,7 +41,7 @@ "----------- append inform with final result ---------------------"; states:=[]; CalcTree [(["TERM ((14 * x * y) / ( x * y ))", "normalform N"], - ("Rational.thy",["rational","simplification"], + ("Rational",["rational","simplification"], ["simplification","of_rationals"]))]; Iterator 1; moveActiveRoot 1; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/system.sml --- a/test/Tools/isac/Knowledge/system.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/system.sml Wed Sep 08 16:47:22 2010 +0200 @@ -47,14 +47,14 @@ val fmz = ["equalities [0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2, 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2]", "solveForVars [c, c_2]", "solution ss___"]; val (dI',pI',mI') = - ("Biegelinie.thy",["normalize","2x2","linear","system"], + ("Biegelinie",["normalize","2x2","linear","system"], ["EqSystem","normalize","2x2"]); val p = e_pos'; val c = []; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -case nxt of (_, Specify_Theory "Biegelinie.thy") => () +case nxt of (_, Specify_Theory "Biegelinie") => () | _ => raise error "system.sml diff.behav.in me --1"; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -67,14 +67,14 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -case nxt of (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", +case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear", "system"])) => () | _ => raise error "system.sml diff.behav.in me --3"; val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -case nxt of (_, Specify_Theory "Biegelinie.thy") => () +case nxt of (_, Specify_Theory "Biegelinie") => () | _ => raise error "system.sml diff.behav.in me --1"; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; diff -r 24609758d219 -r 028442673981 test/Tools/isac/Knowledge/termorder.sml --- a/test/Tools/isac/Knowledge/termorder.sml Wed Sep 08 16:45:27 2010 +0200 +++ b/test/Tools/isac/Knowledge/termorder.sml Wed Sep 08 16:47:22 2010 +0200 @@ -72,7 +72,7 @@ else raise error "termorder.sml diff.behav ord_make_polynomial_in #14"; val SOME (t',_) = - rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp'; + rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp'; (*MG 2003... "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()