(* tests for Complex.thy

 use"../smltest/IsacKnowledge/complex.sml";

 use"complex.sml";

 *)

 val thy = Isac.thy;

 subthy (Float.thy, ComplexI.thy);

  val t = (term_of o the o (parse ComplexI.thy)) "I__";

  atomt t;

  val t = str2term "I__";

  atomt t;

  val t = str2term "1 + 2 * I__";

  atomt t;

  val t = str2term "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";

  atomt t;

 (*andere konkrete Syntax ???*)

  val t = str2term "Float ((1,2),(0,0)) * I__";

  atomt t;

  term2str t;

  val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";

  atomt t;

  term2str t;

  (*---  (1.1 + 2.2 I) * (3.3 + 4.4 I) = - 6.05 + 12 I  ---*)

  val t = str2term "(Float ((11,-1),(0,0)) + Float ((22,-1),(0,0)) * I__) *\

 		 \(Float ((33,-1),(0,0)) + Float ((44,-1),(0,0)) * I__)";

  val SOME (t',_) = 

      rewrite_set_ thy false 

 		  (append_rls "simpl_complex" make_polynomial 

 			      [Thm ("square_I", num_str square_I)]) t;

  term2str t';

  "Float ((363, -2), 0, 0) + I__ * Float ((484, -2), 0, 0) +\

  \I__ * Float ((726, -2), 0, 0) + -1 * Float ((968, -2), 0, 0)"

  (*--- mit dem rls make_polynomial geht ja schon allerhand !!!---*)