1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Complex.thy	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,26 @@
     1.4 +(* imaginary unit, close to traditional notation in algebra systems;
     1.5 +   types questionable, see Isabelle/HOL/Real/Complex_Numbers.thy
     1.6 +
     1.7 +   use_thy_only"knowledge/Complex";
     1.8 +   use_thy_only"Complex";
     1.9 +
    1.10 +   use_thy"knowledge/Complex";
    1.11 +   use_thy"Complex";
    1.12 +   *)
    1.13 +
    1.14 +Complex = Float +
    1.15 +
    1.16 +consts
    1.17 +(* waere auch eine Moeglichkeit
    1.18 +  "I'_'_"      :: "real => real"      ("_ I'_'_" [999] 998)
    1.19 +*)
    1.20 +  "I'_'_"      :: "real"      (*"I'_'_"*)
    1.21 +
    1.22 +rules
    1.23 +(* waere auch eine Moeglichkeit
    1.24 +  add_I		"a I__ + b I__ = (a + b) I__"
    1.25 +  mult_I	"a I__ * b I__ = -1 * a * b"
    1.26 +*)
    1.27 +  square_I      "I__ * I__ = -1"
    1.28 +
    1.29 +end
    1.30 \ No newline at end of file