1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Sep 05 12:40:23 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Sep 07 10:07:13 2011 +0200
     1.3 @@ -1,9 +1,10 @@
     1.4 -(* interpreter for scripts
     1.5 -   (c) Walther Neuper 2000
     1.6 +(* Title:  interpreter for scripts
     1.7 +   Author: Walther Neuper 2000
     1.8 +   (c) due to copyright terms
     1.9 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.10 +        10        20        30        40        50        60        70        80
    1.11 +*)
    1.12  
    1.13 -use"ME/script.sml";
    1.14 -use"script.sml";
    1.15 -*)
    1.16  signature INTERPRETER =
    1.17  sig
    1.18    (*type ets (list of executed tactics) see sequent.sml*)
    1.19 @@ -565,12 +566,12 @@
    1.20  
    1.21    | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
    1.22      (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
    1.23 -      ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
    1.24 +      (tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
    1.25  	     ", consts'= "^(term2str consts'));
    1.26 -       atomty consts; atomty consts';*)
    1.27 +       atomty consts; atomty consts';
    1.28         if consts = consts'
    1.29 -       then ((*tracing"### assod Check'_elementwise: Ass";*) Ass (m, consts_chkd))
    1.30 -       else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
    1.31 +       then (tracing"### assod Check'_elementwise: Ass"; Ass (m, consts_chkd))
    1.32 +       else (tracing"### assod Check'_elementwise: NotAss"; NotAss))
    1.33  
    1.34    | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
    1.35  	    Ass (m, list) 
    1.36 @@ -1224,6 +1225,7 @@
    1.37  	             else Steps (ScrState is, ss))
    1.38  	
    1.39          | NasApp _ => NotLocatable
    1.40 +        | err => (writeln ("*** " ^ PolyML.makestring err); NotLocatable)
    1.41        end
    1.42  
    1.43    | locate_gen _ m _ (sc,_) (is, _) = 

     2.1 --- a/test/Tools/isac/Knowledge/polyeq.sml	Mon Sep 05 12:40:23 2011 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml	Wed Sep 07 10:07:13 2011 +0200
     2.3 @@ -1,11 +1,6 @@
     2.4  (* testexamples for PolyEq, poynomial equations and equational systems
     2.5 -   author: Richard Lang
     2.6 -   2003
     2.7 +   author: Richard Lang 2003  
     2.8     (c) due to copyright terms
     2.9 -
    2.10 -use"../smltest/IsacKnowledge/polyeq.sml";
    2.11 -use"polyeq.sml";
    2.12 -
    2.13  WN030609: some expls dont work due to unfinished handling of 'expanded terms';
    2.14            others marked with TODO have to be checked, too.
    2.15  *)
    2.16 @@ -16,6 +11,8 @@
    2.17  "-----------------------------------------------------------------";
    2.18  "----------- tests on predicates in problems ---------------------";
    2.19  "----------- test matching problems --------------------------0---";
    2.20 +"----------- lin.eq degree_0 -------------------------------------";
    2.21 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
    2.22  "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
    2.23  "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
    2.24  "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
    2.25 @@ -28,110 +25,97 @@
    2.26  "-----------------------------------------------------------------";
    2.27  "-----------------------------------------------------------------";
    2.28  
    2.29 -(*=== inhibit exn ?=============================================================
    2.30 -
    2.31 -val c = []; 
    2.32 +val c = []; print_depth 5;
    2.33  
    2.34  "----------- tests on predicates in problems ---------------------";
    2.35  "----------- tests on predicates in problems ---------------------";
    2.36  "----------- tests on predicates in problems ---------------------";
    2.37  (* 
    2.38 - Compiler.Control.Print.printDepth:=5; (*4 default*)
    2.39   trace_rewrite:=true;
    2.40   trace_rewrite:=false;
    2.41  *)
    2.42   val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
    2.43 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
    2.44 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
    2.45   if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
    2.46   else  error "polyeq.sml: diff.behav. in lhs";
    2.47  
    2.48 -
    2.49   val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
    2.50 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
    2.51 - if (term2str t) = "HOL.True" then ()
    2.52 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
    2.53 + if (term2str t) = "True" then ()
    2.54   else  error "polyeq.sml: diff.behav. 1 in is_expended_in";
    2.55  
    2.56   val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
    2.57 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
    2.58 - if (term2str t) = "HOL.False" then ()
    2.59 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
    2.60 + if (term2str t) = "False" then ()
    2.61   else  error "polyeq.sml: diff.behav. 2 in is_poly_in";
    2.62  
    2.63 -
    2.64   val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
    2.65 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
    2.66 - if (term2str t) = "HOL.True" then ()
    2.67 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
    2.68 + if (term2str t) = "True" then ()
    2.69   else  error "polyeq.sml: diff.behav. 3 in is_poly_in";
    2.70  
    2.71 -
    2.72   val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
    2.73 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
    2.74 - if (term2str t) = "HOL.True" then ()
    2.75 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
    2.76 + if (term2str t) = "True" then ()
    2.77   else  error "polyeq.sml: diff.behav. 4 in is_expended_in";
    2.78  
    2.79  
    2.80   val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
    2.81 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
    2.82 - if (term2str t) = "HOL.True" then ()
    2.83 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
    2.84 + if (term2str t) = "True" then ()
    2.85   else  error "polyeq.sml: diff.behav. 5 in is_expended_in";
    2.86   
    2.87   val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
    2.88 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
    2.89 - if (term2str t) = "HOL.True" then ()
    2.90 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
    2.91 + if (term2str t) = "True" then ()
    2.92   else  error "polyeq.sml: diff.behav. in has_degree_in_in";
    2.93  
    2.94 -
    2.95   val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
    2.96 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
    2.97 - if (term2str t) = "HOL.False" then ()
    2.98 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
    2.99 + if (term2str t) = "False" then ()
   2.100   else  error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
   2.101  
   2.102   val t4 = (term_of o the o (parse thy)) 
   2.103  	      "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
   2.104 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
   2.105 - if (term2str t) = "HOL.False" then ()
   2.106 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
   2.107 + if (term2str t) = "False" then ()
   2.108   else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
   2.109  
   2.110 -
   2.111   val t5 = (term_of o the o (parse thy)) 
   2.112  	      "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
   2.113 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
   2.114 - if (term2str t) = "HOL.True" then ()
   2.115 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
   2.116 + if (term2str t) = "True" then ()
   2.117   else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
   2.118  
   2.119 +"----------- test matching problems --------------------------0---";
   2.120 +"----------- test matching problems --------------------------0---";
   2.121 +"----------- test matching problems --------------------------0---";
   2.122 +val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
   2.123 +if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
   2.124 +  Matches' {Find = [Correct "solutions L"], 
   2.125 +            With = [], 
   2.126 +            Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 
   2.127 +            Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)", 
   2.128 +                     Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"], 
   2.129 +            Relate = []}
   2.130 +then () else error "match_pbl [expanded,univariate,equation]";
   2.131  
   2.132 -"----------- test matching problems --------------------------0---";
   2.133 -"----------- test matching problems --------------------------0---";
   2.134 -"----------- test matching problems --------------------------0---";
   2.135 - val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
   2.136 - val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
   2.137 -     get_pbt ["expanded","univariate","equation"];
   2.138 - 
   2.139 - match_pbl fmz (get_pbt ["expanded","univariate","equation"]);
   2.140 - (*Matches'
   2.141 -    {Find=[Correct "solutions L"],
   2.142 -     Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
   2.143 -            Correct "solveFor x"],Relate=[],
   2.144 -     Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
   2.145 -            Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],With=[]}
   2.146 - *)
   2.147 - match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]);
   2.148 - (*Matches'
   2.149 -    {Find=[Correct "solutions L"],
   2.150 -     Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
   2.151 -            Correct "solveFor x"],Relate=[],
   2.152 -     Where=[Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x =!= 2"],
   2.153 -     With=[]}*)
   2.154 +if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
   2.155 +  Matches' {Find = [Correct "solutions L"], 
   2.156 +            With = [], 
   2.157 +            Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 
   2.158 +            Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"], 
   2.159 +            Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)
   2.160 +then () else error "match_pbl [degree_2,expanded,univariate,equation]";
   2.161  
   2.162 -"-------------------- test thm's degree_0 --------------------------------------";
   2.163 -"-------------------- test thm's degree_0 --------------------------------------";
   2.164 +"----------- lin.eq degree_0 -------------------------------------";
   2.165 +"----------- lin.eq degree_0 -------------------------------------";
   2.166 +"----------- lin.eq degree_0 -------------------------------------";
   2.167  "----- d0_false ------";
   2.168 -(*EP*)
   2.169 -val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
   2.170 +(*=== inhibit exn WN110906 ======================================================
   2.171 +val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
   2.172  val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
   2.173                       ["PolyEq","solve_d0_polyeq_equation"]);
   2.174 -(*val p = e_pos'; 
   2.175 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
   2.176 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
   2.177  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   2.178  val (p,_,f,nxt,_,pt) = me nxt p c pt;
   2.179  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
   2.180 @@ -144,12 +128,9 @@
   2.181  
   2.182  "----- d0_true ------";
   2.183  (*EP-7*)
   2.184 -val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
   2.185 +val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
   2.186  val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
   2.187                       ["PolyEq","solve_d0_polyeq_equation"]);
   2.188 -(*val p = e_pos'; val c = []; 
   2.189 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
   2.190 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
   2.191  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   2.192  val (p,_,f,nxt,_,pt) = me nxt p c pt;
   2.193  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
   2.194 @@ -159,16 +140,13 @@
   2.195  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
   2.196  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
   2.197  	 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
   2.198 +============ inhibit exn WN110906 ============================================*)
   2.199  
   2.200 -"-------------------- test thm's degree_2 ------------------------------------------";
   2.201 -"-------------------- test thm's degree_2 ------------------------------------------";
   2.202 -
   2.203 -"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
   2.204 -"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
   2.205 -"-------------------- test thm's d2_pq_formulsxx[_neg]-----";
   2.206 -
   2.207 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
   2.208 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
   2.209 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
   2.210  "----- d2_pqformula1 ------!!!!";
   2.211 -val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
   2.212 +val fmz = ["equality (-2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
   2.213  val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
   2.214  (*val p = e_pos'; val c = []; 
   2.215  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
   2.216 @@ -186,6 +164,9 @@
   2.217  (*### or2list _ | _
   2.218    ### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
   2.219    ([4],Res)  "[x = 2, x = -1]"    Check_elementwise "Assumptions"*)
   2.220 +
   2.221 +(*============ inhibit exn WN110906 ==============================================
   2.222 +GOON WN110906
   2.223  val (p,_,f,nxt,_,pt) = me nxt p c pt;
   2.224  (*### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
   2.225    ([5],Res)   "[x = 2, x = -1]"   Check_Postcond*)
   2.226 @@ -1178,4 +1159,6 @@
   2.227  val ((pt,p),_) = get_calc 1; show_pt pt;
   2.228  
   2.229  interSteps 1 ([1],Res) (*no Rewrite_Set...*);
   2.230 -===== inhibit exn ?===========================================================*)
   2.231 +
   2.232 +============ inhibit exn WN110906 ==============================================*)
   2.233 +

     3.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Sep 05 12:40:23 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Sep 07 10:07:13 2011 +0200
     3.3 @@ -158,7 +158,7 @@
     3.4  (*use "Knowledge/rateq.sml"            2002*)
     3.5  (*use "Knowledge/rootrat.sml"          2002*)
     3.6  (*use "Knowledge/rootrateq.sml"        2002*)
     3.7 -(*use "Knowledge/polyeq.sml"           2002*)
     3.8 +(*use "Knowledge/polyeq.sml"           part. WN110906: problems with comments*)
     3.9  (*use "Knowledge/rlang.sml"            2002???*)
    3.10    use "Knowledge/calculus.sml"       (*new 2011*)
    3.11    use "Knowledge/trig.sml"

     4.1 --- a/test/Tools/isac/Test_Some.thy	Mon Sep 05 12:40:23 2011 +0200
     4.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Sep 07 10:07:13 2011 +0200
     4.3 @@ -1,23 +1,119 @@
     4.4  (* Title:  run tests on a particular test file
     4.5     Author: Walther Neuper 101001
     4.6     (c) copyright due to lincense terms.
     4.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     4.8 +        10        20        30        40        50        60        70        80
     4.9  *)
    4.10  
    4.11  theory Test_Some imports Isac begin
    4.12  
    4.13 -use"../../../test/Tools/isac/ProgLang/rewrite.sml" 
    4.14 -
    4.15 -
    4.16 -ML{*
    4.17 +text{*
    4.18 +use"../../../test/Tools/isac/Knowledge/polyeq.sml" 
    4.19  *}
    4.20  
    4.21  ML {*
    4.22 +val c = [];
    4.23 +print_depth 5;
    4.24 +*}
    4.25 +
    4.26 +ML {*
    4.27 +"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
    4.28 +"----- d2_pqformula1 ------!!!!";
    4.29 +val fmz = ["equality (-2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
    4.30 +val (dI',pI',mI') = 
    4.31 +  ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], 
    4.32 +   ["PolyEq","solve_d2_polyeq_pq_equation"]);
    4.33 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    4.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.36 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.37 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    4.40 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*f = .. "x = 2 | x = -1", nxt = (". ", Or_to_List)*)
    4.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    4.42 +     (*f = "..[x = 2, x = -1]", nxt = ("..Check_elementwise "Assumptions")*)
    4.43 +*}
    4.44 +ML{*
    4.45 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    4.46 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
    4.47 +val (mI,m) = mk_tac'_ tac; (*m = Check_elementwise "Assumptions"*)
    4.48 +val  Appl m = applicable_in p pt m
    4.49 +*}
    4.50 +ML{*
    4.51 +print_depth 5; PolyML.makestring m
    4.52 +*}
    4.53 +ML{*
    4.54 +val Check_elementwise' (a,b,(c,d)) = m;
    4.55 +term2str a;
    4.56 +term2str c;
    4.57 +terms2str d;
    4.58 +*}
    4.59 +ML{*
    4.60 +print_depth 99; m;
    4.61 +*}
    4.62 +ML{*
    4.63 +*}
    4.64 +ML{*
    4.65 +*}
    4.66 +ML{*
    4.67 +locatetac tac (pt,p)
    4.68 +val it = ("failure", ([], [], (Nd (PblObj {...}, [...]), ([4], ...)))): string * 
    4.69 +*}
    4.70 +ML{* (*error*)
    4.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.72 +
    4.73 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    4.74 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
    4.75 +	 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
    4.76 +
    4.77 +"----- d2_pqformula1_neg ------";
    4.78  
    4.79  *}
    4.80  ML{*
    4.81 -
    4.82 +val xxx = @{theory};
    4.83 +(writeln o PolyML.makestring) xxx;
    4.84 +*}
    4.85 +ML {*
    4.86 +NotLocatable
    4.87 +*}
    4.88 +ML {*
    4.89 +NasApp (e_scrstate,[])
    4.90  *}
    4.91  ML{*
    4.92 +((writeln o PolyML.makestring) xxx; NasApp (e_scrstate,[]))
    4.93 +*}
    4.94 +text{*
    4.95 +*** NasNap 
    4.96 +(Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 
    4.97 +  (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 
    4.98 +    Free ("x", "RealDef.real") $ 
    4.99 +    Free ("2", "RealDef.real")) $ 
   4.100 +  (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 
   4.101 +    (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 
   4.102 +      Free ("x", "RealDef.real") $ 
   4.103 +      Free ("-1", "RealDef.real")) $ 
   4.104 +    Const ("List.list.Nil", "HOL.bool List.list")), 
   4.105 +
   4.106 +[(Free ("e_e", "HOL.bool"), 
   4.107 +    Const ("HOL.disj", "HOL.bool \<Rightarrow> HOL.bool \<Rightarrow> HOL.bool") $ 
   4.108 +      (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 
   4.109 +        Free ("x", "RealDef.real") $ 
   4.110 +        Free ("2", "RealDef.real")) $ 
   4.111 +      (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 
   4.112 +        Free ("x", "RealDef.real") $ 
   4.113 +        Free ("-1", "RealDef.real"))), 
   4.114 +  (Free ("v_v", "RealDef.real"), Free ("x", "RealDef.real")), 
   4.115 +  (Free ("L_L", "HOL.bool List.list"), 
   4.116 +    Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 
   4.117 +      (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 
   4.118 +        Free ("x", "RealDef.real") $ 
   4.119 +        Free ("2", "RealDef.real")) $ 
   4.120 +    (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 
   4.121 +      (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 
   4.122 +        Free ("x", "RealDef.real") $ 
   4.123 +        Free ("-1", "RealDef.real")) $ 
   4.124 +      Const ("List.list.Nil", "HOL.bool List.list")))]) 
   4.125  *}
   4.126  ML{*
   4.127  *}
   4.128 @@ -33,8 +129,8 @@
   4.129  end
   4.130  
   4.131  
   4.132 -(*============ inhibit exn AK110725 ==============================================
   4.133 -============ inhibit exn AK110725 ==============================================*)
   4.134 +(*============ inhibit exn WN110906 ==============================================
   4.135 +============ inhibit exn WN110906 ==============================================*)
   4.136  
   4.137  
   4.138  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.