1.1 --- a/doc-src/isac/jrocnik/Test_Complex.thy	Mon Jul 25 14:19:50 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Complex.thy	Mon Jul 25 17:44:19 2011 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  *}
     1.5  ML {*
     1.6  @{term "Complex 1 2 + Complex 3 4"};
     1.7 +print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
     1.8 +*}
     1.9 +ML {*
    1.10  @{term "Complex 1 2 * Complex 3 4"};
    1.11  @{term "Complex 1 2 - Complex 3 4"};
    1.12  @{term "Complex 1 2 / Complex 3 4"};
    1.13 @@ -21,7 +24,13 @@
    1.14  
    1.15  ML {*
    1.16  val a = @{term "Complex 1 2"};
    1.17 +atomty a;
    1.18 +val a = str2term "Complex 1 2";
    1.19 +atomty a;
    1.20 +*}
    1.21 +ML {*
    1.22  val b = @{term "Complex 3 4"};
    1.23 +val b = str2term "Complex 3 4";
    1.24  (*a + (b::complex); ERROR: term + term*)
    1.25  *}
    1.26  
    1.27 @@ -33,7 +42,7 @@
    1.28  *}
    1.29  ML {*
    1.30  val thm = @{thm "complex_add"};
    1.31 -val t = @{term "Complex 1 2 + Complex 3 4"};
    1.32 +val t = str2term "Complex 1 2 + Complex 3 4";
    1.33  val SOME _ = rewrite_ thy ro er true thm t;
    1.34  val SOME (t', _) = rewrite_ thy ro er true thm t;
    1.35  "Complex (1 + 3) (2 + 4)" = term2str t';
    1.36 @@ -41,21 +50,30 @@
    1.37  
    1.38  subsection {*example 2*}
    1.39  ML {*
    1.40 -val Simplify_complex = append_rls "Simplify_complex" norm_Poly
    1.41 +val Simplify_complex = append_rls "Simplify_complex" e_rls
    1.42    [ Thm  ("complex_add",num_str @{thm complex_add}),
    1.43 -		    Thm  ("complex_mult",num_str @{thm complex_mult})
    1.44 +		    Thm  ("complex_mult",num_str @{thm complex_mult}),
    1.45 +		    Rls_ norm_Poly
    1.46  		  ];
    1.47  *}
    1.48  ML {*
    1.49 -val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};
    1.50 +val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
    1.51 +term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
    1.52 +atomty t;
    1.53  *}
    1.54  ML {*
    1.55 +trace_rewrite := true;
    1.56  val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
    1.57 +trace_rewrite := false;
    1.58 +term2str t = "Complex -12 26";
    1.59 +atomty t;
    1.60  *}
    1.61  ML {*
    1.62 -term2str t
    1.63 +
    1.64  *}
    1.65  ML {*
    1.66 +trace_rewrite := true;
    1.67 +trace_rewrite := false;
    1.68  *}
    1.69  
    1.70  end