1.1 --- a/src/Tools/isac/Build_Isac.thy Sun Jun 30 17:27:34 2013 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Jul 11 16:58:31 2013 +0200
1.3 @@ -36,10 +36,10 @@
1.4 use "Interpret/mathengine.sml"
1.5 *) "~~/src/Tools/isac/Interpret/Interpret"
1.6
1.7 -(* use "xmlsrc/mathml.sml"
1.8 +(* use "xmlsrc/mathml.sml"1491
1.9 use "xmlsrc/datatypes.sml"
1.10 use "xmlsrc/pbl-met-hierarchy.sml"
1.11 - use "xmlsrc/thy-hierarchy.sml"
1.12 + use "xmlsrc/thy-hierarchy.sml"
1.13 use "xmlsrc/interface-xml.sml"
1.14 *) "~~/src/Tools/isac/xmlsrc/xmlsrc"
1.15
1.16 @@ -50,8 +50,13 @@
1.17 use "print_exn_G.sml"
1.18 *) "~~/src/Tools/isac/Frontend/Frontend"
1.19
1.20 + "~~/src/Tools/isac/Knowledge/Build_Thydata"
1.21 +(*============ inhibit exn WN130615 ==============================================
1.22 "~~/src/Tools/isac/Knowledge/Isac"
1.23 -(*============ inhibit exn WN130615 ==============================================
1.24 +"~~/src/Tools/isac/Knowledge/Test" (*Attempt to update loaded theory "Build_Isac"*)
1.25 +"~~/src/Tools/isac/Knowledge/Inverse_Z_Transform" (*Attempt to update loaded theory "Build_Isac"*)
1.26 +"~~/src/Tools/isac/Knowledge/PolyMinus" (*Attempt to update loaded theory "Build_Isac"*)
1.27 +
1.28 "~~/src/Tools/isac/Knowledge/Build_Thydata"
1.29 ============ inhibit exn WN130615 ==============================================*)
1.30
2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Jun 30 17:27:34 2013 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Jul 11 16:58:31 2013 +0200
2.3 @@ -1,4 +1,4 @@
2.4 -(* theory collecting all knowledge defined so far
2.5 +(* theory collecting all knowledge defined for the isac mathengine
2.6 WN.11.00
2.7 *)
2.8
2.9 @@ -134,8 +134,14 @@
2.10 ["Isabelle2011-->12"];
2.11 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
2.12 ["Isabelle2011-->12"];
2.13 +store_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
2.14 + ["Isabelle2011-->12"];
2.15 +store_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
2.16 + ["Isabelle2011-->12"];
2.17 store_isa ["IsacKnowledge","Diff","Rulesets"] ["Isabelle2011-->12"];
2.18 store_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"];
2.19 +
2.20 +store_thy @{theory "Test"} ["Isabelle2011-->12"];
2.21 store_isa ["IsacKnowledge","Test","Theorems"] ["Isabelle2011-->12"];
2.22 store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute
2.23 })
2.24 @@ -145,33 +151,33 @@
2.25 ML {*
2.26 insert_errpats ["diff","differentiate_on_R"]
2.27 ([("chain-rule-diff-both",
2.28 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
2.29 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
2.30 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
2.31 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
2.32 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
2.33 + [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
2.34 + parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
2.35 + parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
2.36 + parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
2.37 + parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
2.38 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
2.39 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list);
2.40
2.41 insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
2.42 ([("fill-d_d-arg",
2.43 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
2.44 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
2.45 ("fill-both-args",
2.46 - parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
2.47 + parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
2.48 ("fill-d_d",
2.49 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
2.50 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
2.51 ("fill-inner-deriv",
2.52 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
2.53 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
2.54 ("fill-all",
2.55 - parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
2.56 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
2.57
2.58 insert_errpats ["simplification","of_rationals"]
2.59 ([("addition-of-fractions",
2.60 - [parse_patt thy "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
2.61 - parse_patt thy "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
2.62 - parse_patt thy "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
2.63 - parse_patt thy "?a + (?b /?c)= (?a + ?b)/ ?c",
2.64 - parse_patt thy "?a + (?b /?c)= (?a * ?b)/ ?c"],
2.65 + [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
2.66 + parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
2.67 + parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
2.68 + parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
2.69 + parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
2.70 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1},
2.71 @{thm rat_add1_assoc}, @{thm rat_add2}, @{thm rat_add2_assoc},
2.72 @{thm rat_add3}, @{thm rat_add3_assoc}])]: errpat list);
2.73 @@ -181,17 +187,17 @@
2.74 (* TODO insert_errpats overwrites instead of appending
2.75 insert_errpats ["simplification","of_rationals"]
2.76 (("cancel", (*see master thesis gdarocy*)
2.77 - [(*a*)parse_patt thy "(?a + ?b)/?a = ?b",
2.78 - (*b*)parse_patt thy "(?a + ?b)/?b = ?a",
2.79 - (*c*)parse_patt thy "(?a + ?b)/(?b + ?c) = ?a / ?c",
2.80 - (*d*)parse_patt thy "(?a + ?c)/(?b + ?c) = ?a / ?b",
2.81 - (*e*)parse_patt thy "(?a + ?c)/(?b + ?c) = ?a / ?c",
2.82 - (*f*)parse_patt thy "(?a + ?b)/(?c + ?a) = ?b / ?c",
2.83 - (*g*)parse_patt thy "(?a*?b + ?c)/?a = ?b + ?c",
2.84 - (*h*)parse_patt thy "(?a*?b + ?c)/?b = ?a + ?c",
2.85 - (*i*)parse_patt thy "(?a + ?b*?c)/?b = ?a + ?c",
2.86 - (*j*)parse_patt thy "(?a + ?b*?c)/?b = ?a + ?b",
2.87 - (*k*)parse_patt thy "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
2.88 + [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",
2.89 + (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",
2.90 + (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",
2.91 + (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",
2.92 + (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",
2.93 + (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",
2.94 + (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",
2.95 + (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",
2.96 + (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",
2.97 + (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",
2.98 + (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
2.99 [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));
2.100
2.101 val fillpats = [
3.1 --- a/src/Tools/isac/Knowledge/Isac.thy Sun Jun 30 17:27:34 2013 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Thu Jul 11 16:58:31 2013 +0200
3.3 @@ -6,8 +6,8 @@
3.4 imports "~~/src/Tools/isac/Frontend/Frontend"
3.5 PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*)
3.6 DiophantEq Inverse_Z_Transform Test
3.7 - (*THIS WAITS UNITL Isabelle2013 (? how include into dependency graph?):
3.8 - GCD_Poly_FP*)
3.9 + (*THIS WAITS UNITL Isabelle2013 (? how include into dependency graph?).....
3.10 + ..... GCD_Poly_FP*)
3.11 begin
3.12
3.13 text {* dependencies alternative to those defined by R.Lang during his thesis:
4.1 --- a/test/Tools/isac/Frontend/interface.sml Sun Jun 30 17:27:34 2013 +0200
4.2 +++ b/test/Tools/isac/Frontend/interface.sml Thu Jul 11 16:58:31 2013 +0200
4.3 @@ -1045,7 +1045,7 @@
4.4 val ((pt,_),_) = get_calc 1;
4.5 val p = get_pos 1 1;
4.6 val (Form f, tac, asms) = pt_extract (pt, p);
4.7 -(*============ inhibit exn WN120316 ==============================================
4.8 +(*============ inhibit exn WN120316 compare 2002--2011 ===========================
4.9 if map term2str asms =
4.10 ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^
4.11 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
4.12 @@ -1054,7 +1054,7 @@
4.13 "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
4.14 andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
4.15 else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*)
4.16 -============ inhibit exn WN120316 ==============================================*)
4.17 +============ inhibit exn WN120316 compare 2002--2011 ===========================*)
4.18 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
4.19 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
4.20 then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
5.1 --- a/test/Tools/isac/Interpret/appl.sml Sun Jun 30 17:27:34 2013 +0200
5.2 +++ b/test/Tools/isac/Interpret/appl.sml Thu Jul 11 16:58:31 2013 +0200
5.3 @@ -43,11 +43,6 @@
5.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.5 show_pt pt;
5.6
5.7 -
5.8 -
5.9 -
5.10 -
5.11 -
5.12 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
5.13 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
5.14 val pIopt = get_pblID (pt,ip);
6.1 --- a/test/Tools/isac/Interpret/calchead.sml Sun Jun 30 17:27:34 2013 +0200
6.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Jul 11 16:58:31 2013 +0200
6.3 @@ -386,32 +386,32 @@
6.4 val ags = isalist2list ags';
6.5 val pI = ["linear","system"];
6.6 val pats = (#ppc o get_pbt) pI;
6.7 -(*---inhibit exn provided by this testcase--------------------------
6.8 +(*============ inhibit exn AK110726 ==============================================
6.9 val xxx - match_ags (theory "EqSystem") pats ags;
6.10 --------------------------------------------------------------------*)
6.11 +============ inhibit exn AK110726 ==============================================*)
6.12 "-c1-----------------------------------------------------";
6.13 "--------------------------step through code match_ags---";
6.14 val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);
6.15 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
6.16 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
6.17 val cy = filter is_copy_named pbt; (*=solution*)
6.18 -(*---inhibit exn provided by this testcase--------------------------
6.19 +(*============ inhibit exn AK110726 ==============================================
6.20 val oris' - matc thy pbt' ags [];
6.21 --------------------------------------------------------------------*)
6.22 +============ inhibit exn AK110726 ==============================================*)
6.23 "-------------------------------step through code matc---";
6.24 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
6.25 (is_copy_named_idstr o free2str) t;
6.26 "---if False:...";
6.27 -(*---inhibit exn provided by this testcase--------------------------
6.28 +(*============ inhibit exn AK110726 ==============================================
6.29 val opt - mtc thy p a;
6.30 --------------------------------------------------------------------*)
6.31 +============ inhibit exn AK110726 ==============================================*)
6.32 "--------------------------------step through code mtc---";
6.33 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
6.34 cterm_of;
6.35 val ttt = (dsc $ var);
6.36 -(*---inhibit exn provided by this testcase--------------------------
6.37 +(*============ inhibit exn AK110726 ==============================================
6.38 cterm_of thy (dsc $ var);
6.39 --------------------------------------------------------------------*)
6.40 +============ inhibit exn AK110726 ==============================================*)
6.41
6.42 "-------------------------------------step through end---";
6.43 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
6.44 @@ -477,7 +477,7 @@
6.45 val ags = isalist2list ags';
6.46 val pI = ["linear","system"];
6.47 val pats = (#ppc o get_pbt) pI;
6.48 -(*---inhibit exn provided by this testcase--------------------------
6.49 +(*============ inhibit exn AK110726 ==============================================
6.50 val xxx - match_ags (theory "EqSystem") pats ags;
6.51 -------------------------------------------------------------------*)
6.52 "-c1-----------------------------------------------------";
6.53 @@ -486,21 +486,21 @@
6.54 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
6.55 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
6.56 val cy = filter is_copy_named pbt; (*=solution*)
6.57 -(*---inhibit exn provided by this testcase--------------------------
6.58 +(*============ inhibit exn AK110726 ==============================================
6.59 val oris' - matc thy pbt' ags [];
6.60 -------------------------------------------------------------------*)
6.61 "-------------------------------step through code matc---";
6.62 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
6.63 (is_copy_named_idstr o free2str) t;
6.64 "---if False:...";
6.65 -(*---inhibit exn provided by this testcase--------------------------
6.66 +(*============ inhibit exn AK110726 ==============================================
6.67 val opt - mtc thy p a;
6.68 -------------------------------------------------------------------*)
6.69 "--------------------------------step through code mtc---";
6.70 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
6.71 cterm_of;
6.72 val ttt = (dsc $ var);
6.73 -(*---inhibit exn provided by this testcase--------------------------
6.74 +(*============ inhibit exn AK110726 ==============================================
6.75 cterm_of thy (dsc $ var);
6.76 -------------------------------------------------------------------*)
6.77 "-------------------------------------step through end---";
7.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Jun 30 17:27:34 2013 +0200
7.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Jul 11 16:58:31 2013 +0200
7.3 @@ -35,7 +35,9 @@
7.4 "--------- build fun check_err_patt ?bdv -------------------------";
7.5 "--------- build fun check_error_patterns ------------------------";
7.6 "--------- embed fun check_error_patterns ------------------------";
7.7 +"--------- build fun get_fillpats --------------------------------";
7.8 "--------- embed fun find_fillpatterns ---------------------------";
7.9 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
7.10 "-----------------------------------------------------------------";
7.11 "-----------------------------------------------------------------";
7.12 "-----------------------------------------------------------------";
7.13 @@ -44,7 +46,6 @@
7.14 "--------- appendFormula: on Res + equ_nrls ----------------------";
7.15 "--------- appendFormula: on Res + equ_nrls ----------------------";
7.16 "--------- appendFormula: on Res + equ_nrls ----------------------";
7.17 -
7.18 val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
7.19 (writeln o term2str) sc;
7.20 val Prog sc = (#scr o get_met) ["Test","solve_linear"];
7.21 @@ -62,15 +63,17 @@
7.22 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
7.23 val ((pt,_),_) = get_calc 1;
7.24 val str = pr_ptree pr_short pt;
7.25 -
7.26 - writeln str;
7.27 -(*============ inhibit exn AK110726 ==============================================
7.28 -(* 2nd string should be the same as 1st one *)
7.29 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. 1 + x + -1 * 2 = 0\n2.3. 1 + (x + -1 * 2) = 0\n2.4. 1 + (x + -2) = 0\n2.5. 1 + (x + -2 * 1) = 0\n2.6. 1 + x + -2 * 1 = 0\n";
7.30 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n";
7.31 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then ()
7.32 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
7.33 -============ inhibit exn AK110726 ==============================================*)
7.34 +if str =
7.35 +(". ----- pblobj -----\n" ^
7.36 +"1. x + 1 = 2\n" ^
7.37 +"2. x + 1 + -1 * 2 = 0\n" ^
7.38 +"2.1. x + 1 + -1 * 2 = 0\n" ^
7.39 +"2.2. 1 + x + -1 * 2 = 0\n" ^
7.40 +"2.3. 1 + (x + -1 * 2) = 0\n" ^
7.41 +"2.4. 1 + (x + -2) = 0\n" ^
7.42 +"2.5. 1 + (x + -2 * 1) = 0\n" ^
7.43 +"2.6. 1 + x + -2 * 1 = 0\n" ) then ()
7.44 +else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
7.45
7.46 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
7.47 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
7.48 @@ -88,13 +91,12 @@
7.49 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
7.50
7.51 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
7.52 -
7.53 -(*============ inhibit exn AK110725 ==============================================
7.54 -(* ERROR: exception Bind raised *)
7.55 +(* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
7.56 +(*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
7.57 val (_,(tac,_,_)::_) = get_calc 1;
7.58 if tac = Rewrite_Set "Test_simplify" then ()
7.59 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
7.60 -============ inhibit exn AK110725 ==============================================*)
7.61 +============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
7.62
7.63 autoCalculate 1 CompleteCalc;
7.64 val ((pt,_),_) = get_calc 1;
7.65 @@ -267,21 +269,34 @@
7.66 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
7.67 val ((pt,_),_) = get_calc 1;
7.68 val str = pr_ptree pr_short pt;
7.69 - writeln str;
7.70
7.71 -(*============ inhibit exn AK110725 ==============================================
7.72 -(* 2nd string should be the same as 1st one *)
7.73 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. 1 + x + -1 * 2 = 0\n2.3. 1 + (x + -1 * 2) = 0\n2.4. 1 + (x + -2) = 0\n2.5. 1 + (x + -2 * 1) = 0\n2.6. 1 + x + -2 * 1 = 0\n";
7.74 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n";
7.75 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then()
7.76 - else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
7.77 -============ inhibit exn AK110725 ==============================================*)
7.78 +(* before AK110725 this was
7.79 +". ----- pblobj -----\n
7.80 +1. x + 1 = 2\n
7.81 +2. x + 1 + -1 * 2 = 0\n
7.82 +2.1. x + 1 + -1 * 2 = 0\n
7.83 +2.2. 1 + x + -1 * 2 = 0\n
7.84 +2.3. 1 + (x + -1 * 2) = 0\n
7.85 +2.4. 1 + (x + -2) = 0\n
7.86 +2.5. 1 + (x + -2 * 1) = 0\n
7.87 +2.6. 1 + x + -2 * 1 = 0\n";
7.88 +*)
7.89 +if str =
7.90 +". ----- pblobj -----\n"^
7.91 +"1. x + 1 = 2\n"^
7.92 +"2. x + 1 + -1 * 2 = 0\n"^
7.93 +"2.1. x + 1 + -1 * 2 = 0\n"^
7.94 +"2.2. 1 + x + -1 * 2 = 0\n"^
7.95 +"2.3. 1 + (x + -1 * 2) = 0\n"^
7.96 +"2.4. 1 + (x + -2) = 0\n"^
7.97 +"2.5. 1 + (x + -2 * 1) = 0\n"^
7.98 +"2.6. 1 + x + -2 * 1 = 0\n" then()
7.99 +else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
7.100
7.101 autoCalculate 1 CompleteCalc;
7.102 val ((pt,pos as (p,_)),_) = get_calc 1;
7.103 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
7.104 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
7.105 -
7.106
7.107 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
7.108 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
7.109 @@ -532,14 +547,7 @@
7.110 spec;
7.111 writeln (itms2str_ ctxt probl);
7.112 writeln (itms2str_ ctxt meth);
7.113 -
7.114 -(*============ inhibit exn AK110725 ==============================================
7.115 -(* ERROR: Argument: istate : istate * Proof.context Reason:
7.116 - Can't unify istate to istate * Proof.context *)
7.117 -writeln (istate2str istate);
7.118 -============ inhibit exn AK110725 ==============================================*)
7.119 -
7.120 -print_depth 3;
7.121 +writeln (istate2str (fst istate));
7.122
7.123 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
7.124 (*081016 NOT necessary (but leave it in Java):*)
7.125 @@ -552,10 +560,7 @@
7.126 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
7.127 val NONE = env;
7.128 val (SOME istate, NONE) = loc;
7.129 -(*============ inhibit exn AK110725 ==============================================
7.130 -(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
7.131 -print_depth 5; writeln (istate2str istate); print_depth 3;
7.132 -============ inhibit exn AK110725 ==============================================*)
7.133 +print_depth 5; writeln (istate2str (fst istate)); print_depth 3;
7.134 (*ScrState ([],
7.135 [], NONE,
7.136 ??.empty, Sundef, false)*)
7.137 @@ -583,7 +588,6 @@
7.138 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
7.139 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
7.140
7.141 -
7.142 "--------- Take as 1st tac, start from exp -----------------------";
7.143 "--------- Take as 1st tac, start from exp -----------------------";
7.144 "--------- Take as 1st tac, start from exp -----------------------";
7.145 @@ -599,10 +603,7 @@
7.146 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
7.147 val NONE = env;
7.148 val (SOME istate, NONE) = loc;
7.149 -(*============ inhibit exn AK110725 ==============================================
7.150 -(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
7.151 -print_depth 5; writeln (istate2str istate); print_depth 3;
7.152 -============ inhibit exn AK110725 ==============================================*)
7.153 +print_depth 5; writeln (istate2str (fst istate)); print_depth 3;
7.154 (*ScrState ([],
7.155 [], NONE,
7.156 ??.empty, Sundef, false)*)
7.157 @@ -628,7 +629,6 @@
7.158 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
7.159 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
7.160
7.161 -
7.162 "--------- init_form, start with <NEW> (CAS input) ---------------";
7.163 "--------- init_form, start with <NEW> (CAS input) ---------------";
7.164 "--------- init_form, start with <NEW> (CAS input) ---------------";
7.165 @@ -887,14 +887,11 @@
7.166 parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
7.167 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
7.168 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
7.169 -
7.170 case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
7.171 | NONE => error "check_error_patterns broken";
7.172
7.173 -
7.174 "--------- embed fun check_error_patterns ------------------------";
7.175 "--------- embed fun check_error_patterns ------------------------";
7.176 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
7.177 "--------- embed fun check_error_patterns ------------------------";
7.178 states:=[];
7.179 CalcTree
7.180 @@ -954,6 +951,65 @@
7.181 ("error pattern #chain-rule-diff-both#", calcstate') => ()
7.182 | _ => error "inform with (positive) check_error_patterns broken"
7.183
7.184 +"--------- build fun get_fillpats --------------------------------";
7.185 +"--------- build fun get_fillpats --------------------------------";
7.186 +"--------- build fun get_fillpats --------------------------------";
7.187 +(*cause for this test was: wrong thy in Build_Thydata.thy in
7.188 + insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)
7.189 +val f_curr = str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
7.190 +val errpatID = "chain-rule-diff-both"
7.191 + val {errpats, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
7.192 +val env =
7.193 + [(str2term "f_f", str2term "x ^^^ 2 + sin (x ^^^ 4)"),
7.194 + (str2term "v_v", str2term "x"),
7.195 + (str2term "f_f'", str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))")]
7.196 + val subst = get_bdv_subst prog env
7.197 + val errpatthms = errpats
7.198 + |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
7.199 + |> map (#3: errpat -> thm list)
7.200 + |> flat;
7.201 +"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
7.202 + (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
7.203 + val thmDeriv = Thm.get_name_hint thm
7.204 + val (part, thyID) = thy_containing_thm thmDeriv
7.205 + val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
7.206 + val Hthm {fillpats, ...} = get_the theID
7.207 + val some = map (get_fillform subst (thm, form) errpatID) fillpats;
7.208 +"~~~~~ fun get_fillform, args:";
7.209 + val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
7.210 + (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
7.211 + val (form', _, _, rewritten) =
7.212 + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
7.213 +"~~~~~ fun rew_sub, args:"; val (thy, i, bdv, tless, rls, put_asm, lrd:lrd list, r, t) =
7.214 + ((Isac()), 1, subst, e_rew_ord, e_rls, false, [], (Trueprop $ pat), form);
7.215 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
7.216 + o Logic.strip_imp_concl) r;
7.217 +(*/-------------catch the planned exception*)
7.218 +(let
7.219 + val r' = Envir.subst_term (Pattern.match thy (lhs, t)
7.220 + (Vartab.empty, Vartab.empty)) r;
7.221 +in 111 end
7.222 +) handle PATTERN (*because only a subterm matches*) => 111;
7.223 +case t of t1 $ t2 =>
7.224 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
7.225 + in
7.226 + if rew2 then (t1 $ t2', asm2, lrd, true) else
7.227 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
7.228 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
7.229 + end;
7.230 +(*catch the planned exception-------------/*)
7.231 +
7.232 +val t1 $ t2 = t;
7.233 +val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2;
7.234 +"~~~~~ fun rew_sub, args:"; val (thy, i, bdv, tless, rls, put_asm, lrd:lrd list, r, t) =
7.235 + (thy, i, bdv, tless, rls, put_asm, (lrd@[R]), r, t2);
7.236 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
7.237 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
7.238 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
7.239 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r';
7.240 +if term2str t' = "cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
7.241 + else error "get_fillpats changed 1"
7.242 +
7.243 "--------- embed fun find_fillpatterns ---------------------------";
7.244 "--------- embed fun find_fillpatterns ---------------------------";
7.245 "--------- embed fun find_fillpatterns ---------------------------";
7.246 @@ -977,7 +1033,7 @@
7.247 "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
7.248 val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
7.249 val pp = par_pblobj pt p
7.250 - val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
7.251 + val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
7.252 val ScrState (env, _, _, _, _, _) = get_istate pt pos
7.253 val subst = get_bdv_subst prog env
7.254 val errpatthms = errpats
7.255 @@ -1036,7 +1092,6 @@
7.256 ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
7.257 then () else error "find_fillpatterns changed 4b";
7.258
7.259 -
7.260 "--------- build fun is_exactly_equal, inputFillFormula ----------";
7.261 "--------- build fun is_exactly_equal, inputFillFormula ----------";
7.262 "--------- build fun is_exactly_equal, inputFillFormula ----------";
7.263 @@ -1117,5 +1172,6 @@
7.264 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
7.265 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
7.266 then () else error "inputFillFormula changed 11";
7.267 +(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
7.268 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
7.269
8.1 --- a/test/Tools/isac/Interpret/mathengine.sml Sun Jun 30 17:27:34 2013 +0200
8.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Jul 11 16:58:31 2013 +0200
8.3 @@ -218,12 +218,10 @@
8.4 val pIopt = get_pblID (pt,ip);
8.5 ip = ([],Res) (*false*);
8.6 val SOME pI = pIopt;
8.7 -(*=== inhibit exn 110718 ? =============================================================
8.8 -
8.9 +(*========== inhibit exn AK110718 ==============================================
8.10 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
8.11 (*^^^^^^^^: Apply_Method without init_form*)
8.12 -
8.13 -===== inhibit exn 110718 ? ===========================================================*)
8.14 +========== inhibit exn AK110718 ==============================================*)
8.15
8.16 "----------- fun step -----------------------------------";
8.17 "----------- fun step -----------------------------------";
8.18 @@ -243,7 +241,7 @@
8.19 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
8.20 "----- step 5: returns tac = ---";
8.21
8.22 -(*========== inhibit exn 110718 =======================================================
8.23 +(*========== inhibit exn AK110718 ==============================================
8.24 2002 stops here as well: TODO review actual arguments:
8.25 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
8.26 "----- step 6: returns tac = ---";
8.27 @@ -252,7 +250,7 @@
8.28 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
8.29 "----- step 8: returns tac = ---";
8.30 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
8.31 -============ inhibit exn 110718 =====================================================*)
8.32 +========== inhibit exn AK110718 ==============================================*)
8.33
8.34
8.35 "----------- fun autocalc -------------------------------";
8.36 @@ -282,13 +280,13 @@
8.37 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
8.38 tracing "----- step 8 ---";
8.39 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
8.40 -(*========== inhibit exn 110628 ================================================
8.41 +(*========== inhibit exn AK110718 ==============================================
8.42 WN110628: Integration does not work, see Knowledge/integrate.sml
8.43
8.44 if str = "end-of-calculation" andalso
8.45 term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
8.46 else error "mathengine.sml -- fun autocalc -- end";
8.47 -============ inhibit exn 110628 ==============================================*)
8.48 +========== inhibit exn AK110718 ==============================================*)
8.49
8.50
8.51 "----------- fun autoCalculate -----------------------------------";
9.1 --- a/test/Tools/isac/Interpret/rewtools.sml Sun Jun 30 17:27:34 2013 +0200
9.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Jul 11 16:58:31 2013 +0200
9.3 @@ -6,10 +6,10 @@
9.4 "--------------------------------------------------------";
9.5 "table of contents --------------------------------------";
9.6 "--------------------------------------------------------";
9.7 -(*============ inhibit exn WN120321 ==============================================
9.8 +(*============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! =================
9.9 "----------- fun make_isab ------------------------------";
9.10 "----------- fun collect_isab_thys ----------------------";
9.11 -============ inhibit exn WN120321 ==============================================*)
9.12 +============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ===============*)
9.13 "----------- fun thy_containing_rls ---------------------";
9.14 "----------- fun thy_containing_cal ---------------------";
9.15 (*============ inhibit exn WN120321 ==============================================
10.1 --- a/test/Tools/isac/Interpret/script.sml Sun Jun 30 17:27:34 2013 +0200
10.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Jul 11 16:58:31 2013 +0200
10.3 @@ -195,59 +195,42 @@
10.4 autoCalculate 1 (Step 1);
10.5 val ((pt, p), _) = get_calc 1; show_pt pt;
10.6 val appltacs = sel_appl_atomic_tacs pt p;
10.7 -
10.8 -(*========== inhibit exn AK110721 ================================================
10.9 -(*(*These SHOULD be the same*)
10.10 - print_depth(999);
10.11 - appltacs;
10.12 - [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
10.13 - Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
10.14 - Calculate "TIMES"];*)
10.15 -
10.16 if appltacs =
10.17 - [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
10.18 - Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
10.19 - Calculate "TIMES"] then ()
10.20 -else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
10.21 -========== inhibit exn AK110721 ================================================*)
10.22 +(* WN130613
10.23 + [Rewrite ("radd_commute", "Test.radd_commute") (*"?m + ?n = ?n + ?m"*),
10.24 + Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), Calculate "TIMES"] *)
10.25 + [Rewrite ("radd_commute", "Test.radd_commute"),
10.26 + Rewrite ("add_assoc", "Groups.semigroup_add_class.add_assoc"), Calculate "TIMES"]
10.27 +then () else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
10.28
10.29 trace_script := true;
10.30 trace_script := false;
10.31 applyTactic 1 p (hd appltacs);
10.32 val ((pt, p), _) = get_calc 1; show_pt pt;
10.33 val appltacs = sel_appl_atomic_tacs pt p;
10.34 +(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
10.35
10.36 -(*(* AK110722 Debugging start*)
10.37 -(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
10.38 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
10.39 val ((pt, _), _) = get_calc cI;
10.40 val p = get_pos cI 1;
10.41 -
10.42 locatetac;
10.43 locatetac tac;
10.44 -locatetac tac;
10.45
10.46 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
10.47 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
10.48 val (mI,m) = mk_tac'_ tac;
10.49 -
10.50 applicable_in p pt m ; (*Appl*)
10.51 -
10.52 member op = specsteps mI; (*false*)
10.53 -
10.54 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
10.55 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
10.56 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
10.57 (mI,m); (*string * tac*)
10.58 ptp (*ptree * pos'*);
10.59 -
10.60 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
10.61 (*val (msg, cs') = solve m (pt, pos);
10.62 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
10.63 -
10.64 m;
10.65 (pt, pos);
10.66 -
10.67 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
10.68 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
10.69
10.70 @@ -259,15 +242,6 @@
10.71 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
10.72 assoc_thy;
10.73
10.74 -(*not finished - error continues in fun generate1*)
10.75 -(* AK110722 Debugging end*)*)
10.76 -(*========== inhibit exn AK110721 ================================================
10.77 -"----- WN080102 these vvv do not work, because locatetac starts the search" ^
10.78 - "1 stac too low";
10.79 -(* AK110722 ERROR: assy: call by ([3], Pbl) *)
10.80 -applyTactic 1 p (hd appltacs);
10.81 -============ inhibit exn AK110721 ==============================================*)
10.82 -
10.83 autoCalculate 1 CompleteCalc;
10.84
10.85 "----------- fun init_form, fun get_stac -------------------------";
11.1 --- a/test/Tools/isac/Interpret/solve.sml Sun Jun 30 17:27:34 2013 +0200
11.2 +++ b/test/Tools/isac/Interpret/solve.sml Thu Jul 11 16:58:31 2013 +0200
11.3 @@ -7,7 +7,6 @@
11.4 uses from Rational.ML: Rrls cancel_p, Rrls cancel
11.5 which in turn
11.6 uses from Poly.ML: Rls make_polynomial, Rls expand_binom
11.7 -
11.8 *)
11.9
11.10 "-----------------------------------------------------------------";
12.1 --- a/test/Tools/isac/Knowledge/atools.sml Sun Jun 30 17:27:34 2013 +0200
12.2 +++ b/test/Tools/isac/Knowledge/atools.sml Thu Jul 11 16:58:31 2013 +0200
12.3 @@ -101,6 +101,9 @@
12.4 "----------- boollist2sum ----------------------------------------";
12.5 "----------- boollist2sum ----------------------------------------";
12.6 "----------- boollist2sum ----------------------------------------";
12.7 +fun lhs (Const ("HOL.eq",_) $ l $ _) = l
12.8 + | lhs t = error("lhs called with (" ^ term2str t ^ ")");
12.9 +"-----------^^^redefined due to overwritten identifier -----------";
12.10 val u_ = str2t "[]";
12.11 val u_ = str2t "[b1 = k - 2*q]";
12.12 val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
13.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Sun Jun 30 17:27:34 2013 +0200
13.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Jul 11 16:58:31 2013 +0200
13.3 @@ -16,6 +16,7 @@
13.4 "-------- compute val rlsthmsNOTisac --------------------";
13.5 "-------- hard-coded val rlsthmsNOTisac -----------------";
13.6 "-------- the_hier (! thehier) (collect_thydata ())------";
13.7 +"-------- retrieve errpats ------------------------------";
13.8 "--------------------------------------------------------";
13.9 "--------------------------------------------------------";
13.10 "--------------------------------------------------------";
13.11 @@ -1090,3 +1091,11 @@
13.12 val it = (): unit
13.13
13.14 *)
13.15 +
13.16 +"-------- retrieve errpats ------------------------------";
13.17 +"-------- retrieve errpats ------------------------------";
13.18 +"-------- retrieve errpats ------------------------------";
13.19 +val {errpats, nrls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
13.20 +case errpats of [("chain-rule-diff-both", _, _)] => ()
13.21 + | _ => error "errpats chain-rule-diff-both changed"
13.22 +
14.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Sun Jun 30 17:27:34 2013 +0200
14.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Jul 11 16:58:31 2013 +0200
14.3 @@ -98,7 +98,7 @@
14.4 Subproblem (Test.thy, [linear, univariate, equation, test]), Safe, true)
14.5 ########## OK*)
14.6 p;
14.7 - writeln(istate2str (get_istate pt ([3],Frm)));
14.8 + writeln(istate2str (fst (get_istate pt ([3],Frm))));
14.9 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
14.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.11 (*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
14.12 @@ -126,7 +126,7 @@
14.13
14.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.15 p;
14.16 - writeln(istate2str (get_istate pt ([3],Res)));
14.17 + writeln(istate2str (fst (get_istate pt ([3],Res))));
14.18 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
14.19 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.20
15.1 --- a/test/Tools/isac/Test_Isac.thy Sun Jun 30 17:27:34 2013 +0200
15.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jul 11 16:58:31 2013 +0200
15.3 @@ -25,7 +25,7 @@
15.4 ("ProgLang/termC.sml")
15.5 ("ProgLang/calculate.sml")
15.6 ("ProgLang/rewrite.sml")
15.7 - ("ProgLang/listC.sml")
15.8 + (*"ProgLang/listC.sml"*)
15.9 ("ProgLang/scrtools.sml")
15.10 ("ProgLang/tools.sml")
15.11
15.12 @@ -55,7 +55,7 @@
15.13 ("xmlsrc/mathml.sml")
15.14 ("xmlsrc/datatypes.sml")
15.15 ("xmlsrc/pbl-met-hierarchy.sml")
15.16 - ("xmlsrc/thy-hierarchy.sml")
15.17 + (*"xmlsrc/thy-hierarchy.sml"*)
15.18 ("xmlsrc/interface-xml.sml")
15.19
15.20 ("Frontend/messages.sml")
15.21 @@ -70,17 +70,17 @@
15.22 ("Knowledge/poly.sml")
15.23 (*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
15.24 IN THIS SEQUENCE: SEE Test_Some2.thy*)
15.25 - ("Knowledge/rational.sml")
15.26 + (*"Knowledge/rational.sml"*)
15.27 ("Knowledge/equation.sml")
15.28 ("Knowledge/root.sml")
15.29 ("Knowledge/lineq.sml")
15.30 - ("Knowledge/rooteq.sml")
15.31 + (*"Knowledge/rooteq.sml"*)
15.32 ("Knowledge/rateq.sml")
15.33 ("Knowledge/rootrateq.sml")
15.34 ("Knowledge/polyeq.sml")
15.35 ("Knowledge/calculus.sml")
15.36 ("Knowledge/trig.sml")
15.37 - ("Knowledge/logexp.sml")
15.38 + (*"Knowledge/logexp.sml"*)
15.39 ("Knowledge/diff.sml")
15.40 ("Knowledge/integrate.sml")
15.41 ("Knowledge/eqsystem.sml")
15.42 @@ -97,8 +97,8 @@
15.43 ("Knowledge/build_thydata.sml")
15.44
15.45 begin
15.46 -
15.47 - ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
15.48 +section {* test ML Code of isac *}
15.49 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
15.50 use "library.sml"
15.51 use "calcelems.sml"
15.52 use "ProgLang/termC.sml"
15.53 @@ -125,28 +125,27 @@
15.54 use "Interpret/ctree.sml" (*!...!see(25)*)
15.55 use "Interpret/ptyps.sml"
15.56 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
15.57 -(*TRICK DOESNÄT WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
15.58 +(*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
15.59 use "Interpret/generate.sml"
15.60 -(*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
15.61 - use "Interpret/calchead.sml" (*part.*)
15.62 +(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
15.63 + ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
15.64 + use "Interpret/calchead.sml"
15.65 use "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
15.66 use "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
15.67 - use "Interpret/script.sml" (*!TODO/part.*)
15.68 - use "Interpret/solve.sml" (*part.*)
15.69 - use "Interpret/inform.sml" (*part.*)
15.70 -(*val it = "--------- embed fun check_error_patterns ------------------------": string
15.71 -:
15.72 -val it = "~~~~~ from inform return val:": string
15.73 - check_error_patterns broken ...CONCERNED WITH thehier
15.74 -*)
15.75 + use "Interpret/script.sml"
15.76 + use "Interpret/solve.sml"
15.77 + use "Interpret/inform.sml"
15.78 +(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
15.79 + ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
15.80 use "Interpret/mathengine.sml" (*!part.*)
15.81 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
15.82 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
15.83 - use "xmlsrc/mathml.sml" (*part.*)
15.84 - use "xmlsrc/datatypes.sml" (*TODO/part.*)
15.85 - use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
15.86 -(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
15.87 -(*val it = "----------- ### thes2file ... Exception- Match raised -----------": string
15.88 + use "xmlsrc/mathml.sml" (*part.*)
15.89 + use "xmlsrc/datatypes.sml" (*TODO/part.*)
15.90 + use "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
15.91 +(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
15.92 +(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
15.93 +val it = "----------- ### thes2file ... Exception- Match raised -----------": string
15.94 :
15.95 val it = "~~~~~ fun thes2file, args:": string
15.96 val p = "../../tmp/": path
15.97 @@ -160,10 +159,11 @@
15.98 use "Frontend/messages.sml"
15.99 use "Frontend/states.sml"
15.100 use "Frontend/interface.sml"
15.101 -(*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
15.102 +(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
15.103 + ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
15.104 use "print_exn_G.sml"
15.105 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
15.106 - ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
15.107 + ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
15.108 use "Knowledge/delete.sml"
15.109 use "Knowledge/descript.sml"
15.110 use "Knowledge/atools.sml"
15.111 @@ -199,15 +199,196 @@
15.112 use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
15.113 use "Knowledge/isac.sml"
15.114 use "Knowledge/build_thydata.sml"
15.115 - ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
15.116 + ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
15.117 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
15.118 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
15.119 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
15.120
15.121 +section {* history of tests *}
15.122 +text {*
15.123 + Systematic regression tests have been introduced to isac development in 2003.
15.124 + Sanity of the regression test suffered from updates following Isabelle development,
15.125 + which mostly exceeded the resources available in isac's development.
15.126 +
15.127 + The survey below shall support to efficiently use the tests for isac
15.128 + on different Isabelle versions. Conclusion in most cases will be:
15.129 +
15.130 + !!! Use most recent tests or go back to the old notebook
15.131 + with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
15.132 +*}
15.133 +
15.134 +subsection {* isac on Isabelle2013 *}
15.135 +subsubsection {* Summary of development *}
15.136 +text {*
15.137 +*}
15.138 +subsubsection {* Run tests *}
15.139 +text {*
15.140 +*}
15.141 +subsubsection {* State of tests *}
15.142 +text {*
15.143 +*}
15.144 +subsubsection {* Changesets of begin and end *}
15.145 +text {*
15.146 +*}
15.147 +
15.148 +subsection {* isac on Isabelle2012 *}
15.149 +subsubsection {* Summary of development *}
15.150 +text {*
15.151 + isac on Isabelle2012 is considered just a transitional stage
15.152 + within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
15.153 + For considerations on the transition see
15.154 + ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
15.155 +*}
15.156 +subsubsection {* Run tests *}
15.157 +text {*
15.158 +$ cd /usr/local/isabisac12/
15.159 +$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
15.160 +$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
15.161 +*}
15.162 +subsubsection {* State of tests *}
15.163 +text {*
15.164 + At least the tests from isac on Isabelle2011 run again.
15.165 + However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
15.166 + in parallel with evaluation.
15.167 +
15.168 + Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
15.169 + yields 69 hits, some of which were already present before Isabelle2002-->2009-2
15.170 + (i.e. on the old notebook from 2002).
15.171 +
15.172 + Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
15.173 + # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
15.174 + # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
15.175 + # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
15.176 + Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
15.177 +
15.178 + Some tests have been re-activated (e.g. error patterns, fill patterns).
15.179 +*}
15.180 +subsubsection {* Changesets of begin and end *}
15.181 +text {*
15.182 + TODO
15.183 + :
15.184 + : isac on Isablle2012
15.185 + :
15.186 + Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
15.187 + User: Walther Neuper <neuper@ist.tugraz.at>
15.188 + Date: 2012-09-24 18:35:13 +0200 (8 months)
15.189 + ------------------------------------------------------------------------------
15.190 + Changeset: 48756 (7443906996a8) merged
15.191 + User: Walther Neuper <neuper@ist.tugraz.at>
15.192 + Date: 2012-09-24 18:15:49 +0200 (8 months)
15.193 +*}
15.194 +
15.195 +subsection {* isac on Isabelle2011 *}
15.196 +subsubsection {* Summary of development *}
15.197 +text {*
15.198 + isac's mathematics engine has been extended by two developments:
15.199 + (1) Isabelle's contexts were introduced by Mathias Lehnfeld
15.200 + (2) "error patterns" were introduced by Gabriella Daroczy
15.201 + Regressions tests have been added for both.
15.202 +*}
15.203 +subsubsection {* Run tests *}
15.204 +text {*
15.205 + $ cd /usr/local/isabisac11/
15.206 + $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
15.207 + $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
15.208 +*}
15.209 +subsubsection {* State of tests *}
15.210 +text {*
15.211 + Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
15.212 + and sometimes give reasons for failing tests.
15.213 + (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
15.214 + work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
15.215 +
15.216 + Tests with functions decomposed for single-stepping are marked with
15.217 + "~~~~~ fun , args:"; val
15.218 +
15.219 + The most signification tests (in particular Frontend/interface.sml) run,
15.220 + however, many "error in kernel" are not caught by an exception.
15.221 + ------------------------------------------------------------------------------
15.222 + After the changeset below Test_Isac worked with check_unsynchronized_ref ():
15.223 + ------------------------------------------------------------------------------
15.224 + Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
15.225 + User: Walther Neuper <neuper@ist.tugraz.at>
15.226 + Date: 2012-08-06 10:38:11 +0200 (11 months)
15.227 +*}
15.228 +subsubsection {* Changesets of begin and end *}
15.229 +text {*
15.230 + isac development was done between these changesets:
15.231 + ------------------------------------------------------------------------------
15.232 + Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
15.233 + User: Walther Neuper <neuper@ist.tugraz.at>
15.234 + Date: 2012-09-24 16:39:30 +0200 (8 months)
15.235 + :
15.236 + : isac on Isablle2011
15.237 + :
15.238 + Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
15.239 + Branch: decompose-isar
15.240 + User: Walther Neuper <neuper@ist.tugraz.at>
15.241 + Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
15.242 + ------------------------------------------------------------------------------
15.243 +*}
15.244 +
15.245 +subsection {* isac on Isabelle2009-2 *}
15.246 +subsubsection {* Summary of development *}
15.247 +text {*
15.248 + In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
15.249 + The update was painful (bridging 7 years of Isabelle development) and cut short
15.250 + due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
15.251 + going on to Isabelle2011 although most of the tests did not run.
15.252 +*}
15.253 +subsubsection {* Run tests *}
15.254 +text {*
15.255 + $ cd /usr/local/isabisac09-2/
15.256 + $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
15.257 + $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
15.258 + NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
15.259 +*}
15.260 +subsubsection {* State of tests *}
15.261 +text {*
15.262 + Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
15.263 + If really necessary, go back to the old notebook with Isabelle2002.
15.264 +*}
15.265 +subsubsection {* Changesets of begin and end *}
15.266 +text {*
15.267 + isac development was done between these changesets:
15.268 + ------------------------------------------------------------------------------
15.269 + Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
15.270 + Branch: decompose-isar
15.271 + User: Marco Steger <m.steger@student.tugraz.at>
15.272 + Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
15.273 + :
15.274 + : isac on Isablle2009-2
15.275 + :
15.276 + Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
15.277 + Branch: isac-from-Isabelle2009-2
15.278 + User: Walther Neuper <neuper@ist.tugraz.at>
15.279 + Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
15.280 + ------------------------------------------------------------------------------
15.281 +*}
15.282 +
15.283 +subsection {* isac on Isabelle2002 *}
15.284 +subsubsection {* Summary of development *}
15.285 +text {*
15.286 + From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
15.287 + of isac's mathematics engine has been implemented.
15.288 +*}
15.289 +subsubsection {* Run tests *}
15.290 +subsubsection {* State of tests *}
15.291 +text {*
15.292 + All tests work on an old notebook (the right PolyML coudn't be upgraded to more
15.293 + recent Linux versions)
15.294 +*}
15.295 +subsubsection {* Changesets of begin and end *}
15.296 +text {*
15.297 + Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
15.298 + see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
15.299 +*}
15.300 +
15.301 end
15.302 (*========== inhibit exn 110628 ================================================
15.303 ============ inhibit exn 110628 ==============================================*)
15.304
15.305 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
15.306 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
15.307 +Pending source file dependencies: "Knowledge/algein.sml"
15.308 + -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
15.309
16.1 --- a/test/Tools/isac/Test_Some.thy Sun Jun 30 17:27:34 2013 +0200
16.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 11 16:58:31 2013 +0200
16.3 @@ -1,13 +1,19 @@
16.4
16.5 theory Test_Some imports Isac
16.6 - uses ("~~/test/Tools/isac/Interpret/calchead.sml")
16.7 + uses ("~~/test/Tools/isac/Interpret/inform.sml")
16.8 begin
16.9 - use "~~/test/Tools/isac/Interpret/calchead.sml"
16.10 + use "~~/test/Tools/isac/Interpret/inform.sml"
16.11
16.12 declare [[show_types]]
16.13 declare [[show_sorts]]
16.14 find_theorems "?a <= ?a"
16.15
16.16 +print_facts
16.17 +print_statement ""
16.18 +print_theory
16.19 +
16.20 +ML {*
16.21 +*}
16.22 ML {* (*==================*)
16.23 *}
16.24 ML {*
16.25 @@ -18,15 +24,17 @@
16.26 *}
16.27 ML {*
16.28 *}
16.29 -ML {*
16.30 -*}
16.31 -ML {* (*/==================\*)
16.32 +ML {* (*==================*)
16.33 *}
16.34 ML {*
16.35 *}
16.36 ML {*
16.37 *}
16.38 -ML {* (*\==================/*)
16.39 +ML {*
16.40 +*}
16.41 +ML {*
16.42 +*}
16.43 +ML {* (*==================*)
16.44 "~~~~~ fun , args:"; val () = ();
16.45
16.46 "~~~~~ to return val:"; val () = ();
16.47 @@ -34,8 +42,8 @@
16.48 *}
16.49 end
16.50
16.51 -(*========== inhibit exn WN1130630 maximum example broken =========================
16.52 -============ inhibit exn WN1130630 maximum example broken =======================*)
16.53 +(*========== inhibit exn WN1130701 broken already in 2009-2 =======================
16.54 +============ inhibit exn WN1130701 broken already in 2009-2 =====================*)
16.55 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
16.56 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
16.57