1.1 --- a/src/Tools/isac/Interpret/tactic.sml Tue Jan 22 11:21:08 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/tactic.sml Tue Jan 22 12:08:32 2019 +0100
1.3 @@ -317,7 +317,7 @@
1.4 tac_ contains results from check in 'fun applicable_in'.
1.5 This is useful for costly results, e.g. from rewriting;
1.6 however, these results might be changed by Scripts like
1.7 - " eq = (Rewrite_Set ansatz_rls False) eql;" ^
1.8 + " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
1.9 " eq = drop_questionmarks eq;" ^
1.10 " eq = (Rewrite_Set equival_trans False) eq;" ^
1.11 TODO.WN120106 ANALOGOUSLY TO Substitute':
2.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Jan 22 11:21:08 2019 +0100
2.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Jan 22 12:08:32 2019 +0100
2.3 @@ -136,14 +136,14 @@
2.4 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
2.5 " (let e_e = (hd o (filterVar m_m)) r_s; " ^
2.6 " t_t = (if 1 < LENGTH r_s " ^
2.7 - " then (SubProblem (DiffApp',[make,function],[no_met]) " ^
2.8 + " then (SubProblem (''DiffApp'',[''make'',''function''],[''no_met'']) " ^
2.9 " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
2.10 " else (hd r_s)); " ^
2.11 " (m_x::real) = " ^
2.12 - "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^
2.13 - " [DiffApp,max_on_interval_by_calculus]) " ^
2.14 + "SubProblem(''DiffApp'',[''on_interval'',''maximum_of'',''function''], " ^
2.15 + " [''DiffApp'',''max_on_interval_by_calculus'']) " ^
2.16 " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
2.17 - " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^
2.18 + " in ((SubProblem (''DiffApp'',[''find_values'',''tool''],[''Isac'',''find_values'']) " ^
2.19 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
2.20 " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) ")]
2.21 \<close>
3.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Tue Jan 22 11:21:08 2019 +0100
3.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Tue Jan 22 12:08:32 2019 +0100
3.3 @@ -112,7 +112,7 @@
3.4 "Script Sortprog (unso :: int xlist) = " ^
3.5 " (let uns = Take (sort unso) " ^
3.6 " in " ^
3.7 - " (Rewrite_Set ''ins_sort ''False) uns" ^
3.8 + " (Rewrite_Set ''ins_sort'' False) uns" ^
3.9 " )")]
3.10 \<close>
3.11 setup \<open>KEStore_Elems.add_mets
4.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Jan 22 11:21:08 2019 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Jan 22 12:08:32 2019 +0100
4.3 @@ -136,7 +136,7 @@
4.4 " (facs::real) = factors_from_solution L_L; "^
4.5 " (eql::real) = Take (num_orig / facs); "^
4.6
4.7 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
4.8 + " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; "^
4.9
4.10 " (eq::bool) = Take (eql = eqr); "^
4.11 (*Maybe possible to use HOLogic.mk_eq ??*)
4.12 @@ -152,7 +152,7 @@
4.13
4.14 " (eq_a::bool) = Take eq; "^
4.15 " eq_a = (Substitute [zzz=z1]) eq; "^
4.16 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
4.17 + " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; "^
4.18 " (sol_a::bool list) = "^
4.19 " (SubProblem (''Isac'', "^
4.20 " [''univariate'',''equation''],[''no_met'']) "^
5.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Jan 22 11:21:08 2019 +0100
5.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Jan 22 12:08:32 2019 +0100
5.3 @@ -539,7 +539,7 @@
5.4 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
5.5 " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^
5.6 " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
5.7 - " [no_met]) [BOOL e_e, REAL v_v])))")]
5.8 + " [''no_met'']) [BOOL e_e, REAL v_v])))")]
5.9 \<close>
5.10 setup \<open>KEStore_Elems.add_mets
5.11 [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID
5.12 @@ -585,9 +585,9 @@
5.13 " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
5.14 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
5.15 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
5.16 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
5.17 + " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
5.18 " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^
5.19 - " [no_met]) [BOOL e_e, REAL v_v])))")]
5.20 + " [''no_met'']) [BOOL e_e, REAL v_v])))")]
5.21 \<close>
5.22 (*-- left 28.08.02 --*)
5.23 setup \<open>KEStore_Elems.add_mets
6.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jan 22 11:21:08 2019 +0100
6.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jan 22 12:08:32 2019 +0100
6.3 @@ -172,7 +172,7 @@
6.4 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] " ^
6.5 " ''rootrat_solve'' False))) e_e " ^
6.6 " in (SubProblem (''RootEq'',[''univariate'',''equation''], " ^
6.7 - " [no_met]) [BOOL e_e, REAL v_v]))")]
6.8 + " [''no_met'']) [BOOL e_e, REAL v_v]))")]
6.9 \<close>
6.10
6.11 setup \<open>KEStore_Elems.add_calcs
7.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Jan 22 11:21:08 2019 +0100
7.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Jan 22 12:08:32 2019 +0100
7.3 @@ -521,13 +521,13 @@
7.4 autoCalculate 1 (Step 1);
7.5 getTactic 1 ([1], Frm) (*still empty*);
7.6
7.7 -fetchProposedTactic 1 (*Rewrite_Set_Inst integration_rules*);
7.8 +fetchProposedTactic 1 (*Rewrite_Set_Inst ''integration_rules''*);
7.9 autoCalculate 1 (Step 1);
7.10
7.11 -fetchProposedTactic 1 (*Rewrite_Set_Inst add_new_c*);
7.12 +fetchProposedTactic 1 (*Rewrite_Set_Inst ''add_new_c''*);
7.13 autoCalculate 1 (Step 1);
7.14
7.15 -fetchProposedTactic 1 (*Rewrite_Set_Inst simplify_Integral*);
7.16 +fetchProposedTactic 1 (*Rewrite_Set_Inst ''simplify_Integral''*);
7.17 autoCalculate 1 (Step 1);
7.18
7.19 autoCalculate 1 CompleteCalc;
8.1 --- a/test/Tools/isac/Knowledge/integrate.thy Tue Jan 22 11:21:08 2019 +0100
8.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Tue Jan 22 12:08:32 2019 +0100
8.3 @@ -16,9 +16,9 @@
8.4 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
8.5 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
8.6 "Script IntegrationScript (f_f::real) (v_v::real) = \
8.7 - \ (((Rewrite_Set_Inst [(''bdv'',v_v)] integration_rules False) @@ \
8.8 - \ (Rewrite_Set_Inst [(''bdv'',v_v)] add_new_c False) @@ \
8.9 - \ (Rewrite_Set_Inst [(''bdv'',v_v)] simplify_Integral False)) (f_f::real))")]
8.10 + \ (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@ \
8.11 + \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@ \
8.12 + \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))")]
8.13 \<close>
8.14
8.15 end
9.1 --- a/zcoding-to-test.sh Tue Jan 22 11:21:08 2019 +0100
9.2 +++ b/zcoding-to-test.sh Tue Jan 22 12:08:32 2019 +0100
9.3 @@ -7,5 +7,5 @@
9.4 cd ../../../ # go back to ~~/.
9.5
9.6 # immediately go to testing
9.7 -./bin/isabelle jedit -l Isac test/Tools/isac/Test_Some.thy &
9.8 -#./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
9.9 +#./bin/isabelle jedit -l Isac test/Tools/isac/Test_Some.thy &
9.10 +./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &