(* theory Test_Complex imports Isac begin

 ERROR TODO                     ^^^^:

 ML {*

 @{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

 *)

 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"};

 *}

 ML {*

 val a = @{term "Complex 1 2"};

 val b = @{term "Complex 3 4"};

 (*a + (b::complex); ERROR: term + term*)

 *}

 ML {*

 @{term "let a = Complex 1 2; b = Complex 3 4 in a + b"};

 *}

 ML {*

 (*TODO rules for simplification*)

 *}

 end