src/Pure/isac/IsacKnowledge/ComplexI.ML
branchisac-from-Isabelle2009-2
changeset 37871 875b6efa7ced
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/isac/IsacKnowledge/ComplexI.ML	Wed Jul 21 13:53:39 2010 +0200
     1.3 @@ -0,0 +1,22 @@
     1.4 +(*Komplexe Zahlen, anders als von Isabelle vorgeschlagen,
     1.5 +  und naeher an der traditionellen Schreibweise (sh.auch Mathematica)*)
     1.6 +
     1.7 +
     1.8 +(*---- solche Tests gehoeren nach kbtest/complex.sml ---
     1.9 + val t = (term_of o the o (parse thy)) "I__";
    1.10 + atomt t;
    1.11 + val t = (term_of o the o (parse thy)) "1 + 2 * I__";
    1.12 + atomt t;
    1.13 + val t = (term_of o the o (parse thy)) 
    1.14 +	     "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";
    1.15 + atomt t;
    1.16 +(*andere konkrete Syntax ???*)
    1.17 +
    1.18 + val t = (term_of o the o (parse thy)) "Float ((1,2),(0,0)) * I__";
    1.19 + atomt t;
    1.20 + (*term2str t;*)
    1.21 + val t = (term_of o the o (parse thy)) 
    1.22 +	     "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
    1.23 + atomt t;
    1.24 + (*term2str t;*)
    1.25 +---------------------------------------------------------*)
    1.26 \ No newline at end of file