wneuper/isac: src/sml/systest/scriptnew.sml@90390fecbe74

     1 (* use"../tests/scriptnew.sml";

     2    use"tests/scriptnew.sml";

     3    *)

     5 (*contents*)

     6 " --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

     7 " --- test  9.5.02 Testeq: While Try Repeat @@ ------------------ ";

     8 " --- test 11.5.02 Testeq: let e_ =... in [e_] ------------------ ";

     9 " _________________ me + nxt_step from script ___________________ ";

    10 " _________________ me + sqrt-equ-test: 1.norm_equation  ________ ";

    11 " _________________ equation with x =(-12)/5, but L ={} ------- ";

    12 (*contents*)

    17 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    18 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    19 "  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

    20 store_pbt

    21  (prep_pbt Test.thy

    22  (["tests"],

    23   []:(string * string list) list,

    24   e_rls, None, []));

    25 store_pbt

    26  (prep_pbt Test.thy

    27  (["met-testterm","tests"],

    28   [("#Given" ,["realTestGiven g_"]),

    29    ("#Find"  ,["realTestFind f_"])

    30   ],

    31   e_rls, None, []));

    32 methods:= overwritel (!methods,

    33 [ prep_met (*test for simplification*)

    34  (("Test.thy","met-testterm"):metID,

    35   [("#Given" ,["realTestGiven g_"]),

    36    ("#Find"  ,["realTestFind f_"])

    37    ],

    38    {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

    39     asm_rls=[],asm_thm=[]},

    40  "Script Testterm (g_::real) =   \

    41  \Repeat\

    42  \  ((Repeat (Rewrite rmult_1 False)) Or\

    43  \   (Repeat (Rewrite rmult_0 False)) Or\

    44  \   (Repeat (Rewrite radd_0 False))) g_"

    45  )]);

    46 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];

    47 val (dI',pI',mI') = ("Test.thy",["met-testterm","tests"],

    48 		     ("Test.thy","met-testterm"));

    49 val p = e_pos'; val c = [];

    50 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

    51 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;

    52 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    53 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    57 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met-testterm"))*)

    58 (*----script 111 ------------------------------------------------*)

    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    60 (*"(#0 + #0) * (#1 * (#1 * a))"  nxt= Rewrite ("rmult_1",*)

    61 (*----script 222 ------------------------------------------------*)

    62 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    63 (*"(#0 + #0) * (#1 * a)"         nxt= Rewrite ("rmult_1",*)

    64 (*----script 333 ------------------------------------------------*)

    65 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    66 (*"(#0 + #0) * a"                nxt= Rewrite ("radd_0",*)

    67 (*----script 444 ------------------------------------------------*)

    68 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    69 (*"#0 * a"*)

    70 (*----script 555 ------------------------------------------------*)

    71 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    72 (*"#0"*)

    73 if p=([4],Res) then ()

    74 else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));

    75 (*----script 666 ------------------------------------------------*)

    76 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    77 (*"#0"*)

    78 if nxt=("End_Proof'",End_Proof') then ()

    79 else raise error "new behaviour in 30.4.02 Testterm: End_Proof";

    85 "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

    86 "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

    87 "  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

    88 store_pbt

    89  (prep_pbt Test.thy

    90  (["met-testeq","tests"],

    91   [("#Given" ,["boolTestGiven e_"]),

    92    ("#Find"  ,["boolTestFind v_i_"])

    93   ],

    94   e_rls, None, []));

    95 methods:= overwritel (!methods,

    96 [

    97  prep_met

    98  (("Test.thy","testeq1"):metID,

    99    [("#Given",["boolTestGiven e_"]),

   100    ("#Where" ,[]),

   101    ("#Find"  ,["boolTestFind v_i_"])

   102    ],

   103    {rew_ord'="tless_true",rls'=tval_rls,

   104     srls=append_rls "testeq1_srls" e_rls

   105 		    [Calc ("Test.contains'_root", eval_contains_root"")],

   106     prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]},

   107  "Script Testeq (e_::bool) =                                        \

   108    \(While (contains_root e_) Do                                     \

   109    \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \

   110    \  (Try (Repeat (Rewrite square_equation_left True))) @@ \

   111    \  (Try (Repeat (Rewrite radd_0 False)))))\

   112    \ e_"

   113  )

   114 ]);

   116 val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",

   117 	   "boolTestFind v_i_"];

   118 val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"],

   119 		     ("Test.thy","testeq1"));

   120 val Script sc = (#scr o get_met) ("Test.thy","testeq1");

   121 atomt sc;

   122 val p = e_pos'; val c = [];

   123 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   124 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;

   125 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   126 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   127 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   128 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   129 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   130 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)

   131 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   132 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   133 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   134 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))

   135 val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*)

   136 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   138 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   139 (*** No such constant: "Test.contains'_root"  *)

   141 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   142 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso

   143    nxt=("End_Proof'",End_Proof') then ()

   144 else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";

   149 " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";

   150 " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";

   151 " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";

   152 methods:= overwritel (!methods,

   153 [

   154  prep_met

   155  (("Test.thy","testlet"):metID,

   156    [("#Given",["boolTestGiven e_"]),

   157    ("#Where" ,[]),

   158    ("#Find"  ,["boolTestFind v_i_"])

   159    ],

   160    {rew_ord'="tless_true",rls'=tval_rls,

   161     srls=append_rls "testlet_srls" e_rls

   162 		    [Calc ("Test.contains'_root",eval_contains_root"")],

   163     prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]},

   164    "Script Testeq2 (e_::bool) =                                        \

   165    \(let e_ =\

   166    \  ((While (contains_root e_) Do                                     \

   167    \   (Rewrite square_equation_left True))\

   168    \   e_)\

   169    \in [e_::bool])"

   170    )

   171  ]);

   172 val Script sc = (#scr o get_met) ("Test.thy","testlet");

   173 writeln(term2str sc);

   174 val fmz = ["boolTestGiven (sqrt a = 0)",

   175 	   "boolTestFind v_i_"];

   176 val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"],

   177 		     ("Test.thy","testlet"));

   178 val p = e_pos'; val c = [];

   179 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   180 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;

   181 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   182 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   183 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   184 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   185 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   186 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)

   187 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   188 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   189 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   190 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso

   191    nxt=("End_Proof'",End_Proof') then ()

   192 else raise error "different behaviour in test 11.5.02 Testeq: let e_ =... in [e_]";

   197 " _________________ me + nxt_step from script _________________ ";

   198 " _________________ me + nxt_step from script _________________ ";

   199 " _________________ me + nxt_step from script _________________ ";

   200 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   201 	   "solveFor x","errorBound (eps=0)",

   202 	   "solutions L"];

   203 val (dI',pI',mI') =

   204   ("Test.thy",["sqroot-test","univariate","equation","test"],

   205    ("Test.thy","sqrt-equ-test"));

   206 val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");

   207 writeln(term2str sc);

   209 val p = e_pos'; val c = [];

   210 "--- s1 ---";

   211 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   212 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

   213 "--- s2 ---";

   214 (* val nxt =

   215   ("Add_Given",

   216    Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)

   217 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   218 "--- s3 ---";

   219 (* val nxt = ("Add_Given",Add_Given "solveFor x");*)

   220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   221 "--- s4 ---";

   222 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)

   223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   224 "--- s5 ---";

   225 (* val nxt = ("Add_Find",Add_Find "solutions L");*)

   226 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   227 "--- s6 ---";

   228 (* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*)

   229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   230 "--- s7 ---";

   231 (* val nxt =

   232   ("Specify_Problem",

   233    Specify_Problem ["sqroot-test","univariate","equation","test"]);*)

   234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   235 "--- s8 ---";

   236 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)

   237 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   238 "--- s9 ---";

   239 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)

   240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   241 "--- 1 ---";

   242 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)

   243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   244 "--- 2 ---";

   245 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   246 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   247 "--- 3 ---";

   248 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)

   249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   250 "--- 4 ---";

   251 (* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)

   252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   253 "--- 5 ---";

   254 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   256 "--- 6 ---";

   257 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)

   258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   259 "--- 7 ---";

   260 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   262 "--- 8<> ---";

   263 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)

   264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   265 "--- 9<> ---";

   266 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   267 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   268 "--- 10<> ---";

   269 (* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)

   270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   271 "--- 11<> ---";

   272 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   273 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   274 "--- 12<> ---.";

   275 (* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)

   276 get_form nxt p pt;

   277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   278 "--- 13<> ---";

   279 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   281 "--- 14<> ---";

   282 (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)

   283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   284 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))

   285 then raise error "scriptnew.sml 1: me + msteps from script: new behaviour"

   286 else ();

   287 "--- 15<> ---";

   288 (* val nxt = ("End_Proof'",End_Proof');*)

   289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   291 writeln (pr_ptree pr_short pt);

   292 writeln("result: "^(get_obj g_result pt [])^

   293 "\n=============================================================");

   294 (*get_obj g_asm pt [];

   295 val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)

   301 " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

   302 " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

   303 " _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

   304 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   305 	   "solveFor x","errorBound (eps=0)",

   306 	   "solutions L"];

   307 val (dI',pI',mI') =

   308   ("Test.thy",["sqroot-test","univariate","equation","test"],

   309    ("Test.thy","sqrt-equ-test"));

   310  val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");

   311  (writeln o term2str) sc;

   312 val p = e_pos'; val c = [];

   313 "--- s1 ---";

   314 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   315 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

   316 "--- s2 ---";

   317 (* val nxt = ("Add_Given",

   318    Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)

   319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   320 "--- s3 ---";

   321 (* val nxt = ("Add_Given",Add_Given "solveFor x");*)

   322 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   323 "--- s4 ---";

   324 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)

   325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   326 "--- s5 ---";

   327 (* val nxt = ("Add_Find",Add_Find "solutions L");*)

   328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   329 "--- s6 ---";

   330 (* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*)

   331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   332 "--- s7 ---";

   333 (* val nxt = ("Specify_Problem",

   334    Specify_Problem ["sqroot-test","univariate","equation","test"]);*)

   335 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   336 "--- s8 ---";

   337 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)

   338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   339 "--- s9 ---";

   340 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)

   341 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   342 "--- !!! x1 --- 1.norm_equation";

   343 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");

   344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   345 "--- !!! x2 --- 1.norm_equation";

   346 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   347 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   348 (*(me nxt p [1] pt) handle e => print_exn_G e;*)

   349 "--- !!! x3 --- 1.norm_equation";

   350 (*val nxt = ("Empty_Mstep",Empty_Mstep) ### helpless*)

   351 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

   352 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   353 "--- !!! x4 --- 1.norm_equation";

   354 (*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)

   355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   356 "--- !!! x5 --- 1.norm_equation";

   357 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

   358 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   359 if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))

   360 then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test";

   363 (* use"../tests/scriptnew.sml";

   364    *)

   366 " _________________ equation with x =(-12)/5, but L ={} ------- ";

   368 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",

   369 	   "solveFor x","errorBound (eps=0)",

   370 	   "solutions L"];

   371 val (dI',pI',mI') =

   372   ("Test.thy",["sqroot-test","univariate","equation","test"],

   373    ("Test.thy","square_equation"));

   374 val p = e_pos'; val c = [];

   375 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   376 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

   377 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   378 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   379 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   380 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   381 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   382 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   383 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   388 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   389 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   390 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   391 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   396 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   404 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   409 trace_rewrite:=true;

   410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   412 trace_rewrite:=false;

   414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   415 val Form' (FormKF (_,_,_,_,ff)) = f;

   416 if ff="[]" then ()

   417 else raise error "diff.behav. in scriptnew.sml; root-eq: L = []";

   420 val tt = (term_of o the o (parse thy)) "?xxx";

   421 rewrite_set_ thy true tval_rls ;

author	agriesma
	Thu, 17 Apr 2003 18:01:03 +0200
branch	griesmayer
changeset 338	90390fecbe74
child 710	afa379bfb2c6
permissions	-rw-r--r--