diff -r e9cb13460b88 -r dc2fe21d2183 doc-src/isac/jrocnik/Test_Complex.thy
--- a/doc-src/isac/jrocnik/Test_Complex.thy	Fri Jul 22 10:26:39 2011 +0200
+++ b/doc-src/isac/jrocnik/Test_Complex.thy	Fri Jul 22 12:10:13 2011 +0200
@@ -1,33 +1,61 @@
-(* theory Test_Complex imports Isac begin
-ERROR TODO                     ^^^^:
+theory Test_Complex imports Isac begin
+
+section {*terms and operations*}
 ML {*
-@{term "Complex 1 2 ^ Complex 3 4"};
+print_depth 999; @{term "Complex 1 (2::real)"};
 *}
-Type unification failed: Clash of types "complex" and "nat"
-Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
-Operand:   Complex 3 4 :: complex
-*)
-
-theory Test_Complex imports Main begin
-
 ML {*
-@{term "Complex 1 2"};
 @{term "Complex 1 2 + Complex 3 4"};
 @{term "Complex 1 2 * Complex 3 4"};
 @{term "Complex 1 2 - Complex 3 4"};
 @{term "Complex 1 2 / Complex 3 4"};
-@{term "Complex 1 2 ^ Complex 3 4"};
+(*@{term "Complex 1 2 ^ Complex 3 4"};
+  Type unification failed: Clash of types "complex" and "nat"
+  Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
+  Operand:   Complex 3 4 :: complex*)
 *}
 ML {*
+term2str @{term "Complex 1 2 + Complex 3 4"};
+term2str @{term "Complex 1 2 / Complex 3 4"};
+*}
+
+ML {*
 val a = @{term "Complex 1 2"};
 val b = @{term "Complex 3 4"};
 (*a + (b::complex); ERROR: term + term*)
 *}
+
+section {*use the operations for simplification*}
+subsection {*example 1*}
 ML {*
-@{term "let a = Complex 1 2; b = Complex 3 4 in a + b"};
+print_depth 1;
+val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
 *}
 ML {*
-(*TODO rules for simplification*)
+val thm = @{thm "complex_add"};
+val t = @{term "Complex 1 2 + Complex 3 4"};
+val SOME _ = rewrite_ thy ro er true thm t;
+val SOME (t', _) = rewrite_ thy ro er true thm t;
+"Complex (1 + 3) (2 + 4)" = term2str t';
+*}
+
+subsection {*example 2*}
+ML {*
+val Simplify_complex = append_rls "Simplify_complex" norm_Poly
+  [ Thm  ("complex_add",num_str @{thm complex_add}),
+		    Thm  ("complex_mult",num_str @{thm complex_mult})
+		  ];
+*}
+ML {*
+val t = @{term "0 * (Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))"};
+*}
+ML {*
+val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
+*}
+ML {*
+term2str t
+*}
+ML {*
 *}
 
 end