1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Tue Jul 26 14:00:38 2011 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Tue Jul 26 14:35:06 2011 +0200
     1.3 @@ -324,8 +324,6 @@
     1.4  term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
     1.5  (*checked visually: trace_rewrite looks like above for 2009*)
     1.6  
     1.7 -trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
     1.8 -(*show_types := false;*)
     1.9  writeln "----- rewrite_ rat_mult_poly_r--------------------------";
    1.10  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
    1.11  (*t' = t''; (*false because of further rewrites in t'*)*)
    1.12 @@ -336,36 +334,11 @@
    1.13  val cond = @{term "(x / x ^^^ 2)"};
    1.14  val NONE = rewrite_set_ thy true erls cond; 
    1.15  (* ^^^^^ goes with '======  calc. to: False' above from beginning*)
    1.16 -trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
    1.17 -"--------------------------------------------------------";
    1.18 +
    1.19  
    1.20  "----------- compare all prepat's existing 2010 ---------";
    1.21  "----------- compare all prepat's existing 2010 ---------";
    1.22  "----------- compare all prepat's existing 2010 ---------";
    1.23 -(* Christian Urban, 101001 
    1.24 -theory Test
    1.25 -imports Main Complex
    1.26 -begin
    1.27 -
    1.28 -let
    1.29 -  val parser = Args.context -- Scan.lift Args.name_source
    1.30 -  fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
    1.31 -  |> ML_Syntax.print_term |> ML_Syntax.atomic
    1.32 -in
    1.33 -  ML_Antiquote.inline "term_pat" (parser >> term_pat)
    1.34 -end
    1.35 -
    1.36 -  val t = @{term "a + b * x = (0 ::real)"};
    1.37 -  val pat = @{term_pat "?l = (?r ::real)"};
    1.38 -  val precond = @{term_pat "is_polynomial (?l::real)"};
    1.39 -  val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
    1.40 -
    1.41 -  Envir.subst_term inst precond
    1.42 -  |> Syntax.string_of_term @{context}
    1.43 -  |> writeln
    1.44 -
    1.45 -
    1.46 -end *)
    1.47  val thy = @{theory "Isac"};
    1.48  val t = @{term "a + b * x = (0 ::real)"};
    1.49  val pat = parse_patt thy "?l = (?r ::real)";