test/Tools/isac/ProgLang/rewrite.sml
branchdecompose-isar
changeset 41943 f33f6959948b
parent 41942 72187c16c796
child 42188 f7b348d64d0c
     1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Sat Mar 19 15:18:10 2011 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Wed Mar 23 17:20:39 2011 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4  "--------------------------------------------------------";
     1.5  "--------------------------------------------------------";
     1.6  
     1.7 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     1.8  
     1.9  "----------- assemble rewrite ---------------------------";
    1.10  "----------- assemble rewrite ---------------------------";
    1.11 @@ -54,7 +55,6 @@
    1.12  (*lookup in isabelle?trace?response...*)
    1.13  writeln(Syntax.string_of_term ctxt rew);
    1.14  writeln(Syntax.string_of_term ctxt RHS);
    1.15 -
    1.16  "===== rewriting: prep insertion into rew_sub";
    1.17  val thy = @{theory Complex_Main};
    1.18  val ctxt = @{context};
    1.19 @@ -504,7 +504,6 @@
    1.20  scan_ chk prepat;
    1.21  tracing "=== poly.sml: scan_ chk prepat end";
    1.22  
    1.23 -
    1.24  "----- chk ---";
    1.25  (*reestablish...*) val t = str2term "x ^^^ 2 * x";
    1.26  val [(pres, pat)] = prepat;
    1.27 @@ -524,5 +523,4 @@
    1.28      ([], true) => ()
    1.29    | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
    1.30  
    1.31 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.32  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)