diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/Test_Complex.thy
--- a/src/Doc/isac/jrocnik/Test_Complex.thy	Mon Sep 16 12:27:20 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-theory Test_Complex imports Isac begin
-
-section {*terms and operations*}
-ML {*
-  print_depth 999; @{term "Complex 1 (2::real)"};
-*}
-ML {*
-@{term "Complex 1 2 + Complex 3 4"};
-print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
-*}
-ML {*
-@{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"};
-atomty a;
-val a = str2term "Complex 1 2";
-atomty a;
-*}
-ML {*
-val b = @{term "Complex 3 4"};
-val b = str2term "Complex 3 4";
-(*a + (b::complex); ERROR: term + term*)
-*}
-
-section {*use the operations for simplification*}
-
-
-
-subsection {*example 1 -- ADD*}
-ML {*
-  print_depth 1;
-  val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
-*}
-ML {*
-  val thm = @{thm "complex_add"};
-  val t = str2term "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 -- ADD, MULT*}
-ML {*
-
-val Simplify_complex = append_rls "Simplify_complex" e_rls
-  [ Thm  ("complex_add",num_str @{thm complex_add}),
-		    Thm  ("complex_mult",num_str @{thm complex_mult}),
-		    Rls_ norm_Poly
-		  ];
-
-*}
-ML {*
-
-val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
-term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
-atomty t;
-
-*}
-ML {*
-
-
-val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
-
-term2str t = "Complex -12 26";
-atomty t;
-
-*}
-
-subsection {*example 3*}
-ML {*
-val Simplify_complex = append_rls "Simplify_complex" e_rls
-  [ Thm  ("complex_mult",num_str @{thm complex_mult}),
-    Thm  ("complex_inverse",num_str @{thm complex_inverse}),
-		    Rls_ norm_Poly
-		  ];
-*}
-ML {*
-val t = str2term "inverse (Complex (2::real) (4::real))";
-term2str t = "inverse Complex (2) (4)";
-atomty t;
-*}
-ML {*
-trace_rewrite := true;
-val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
-trace_rewrite := false;
-term2str t = "Complex -12 26";
-atomty t;
-*}
-
-
-
-ML {*
-trace_rewrite := true;
-trace_rewrite := false;
-*}
-
-end
-