1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Calculus.thy	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,4 @@
     1.4 +
     1.5 +Calculus = Real +
     1.6 +
     1.7 +end
     1.8 \ No newline at end of file

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/sml/IsacKnowledge/Complex.ML	Thu Apr 17 18:01:03 2003 +0200
     2.3 @@ -0,0 +1,22 @@
     2.4 +(*Komplexe Zahlen, anders als von Isabelle vorgeschlagen,
     2.5 +  und naeher an der traditionellen Schreibweise (sh.auch Mathematica)*)
     2.6 +
     2.7 +
     2.8 +(*---- solche Tests gehoeren nach kbtest/complex.sml ---
     2.9 + val t = (term_of o the o (parse thy)) "I__";
    2.10 + atomt t;
    2.11 + val t = (term_of o the o (parse thy)) "1 + 2 * I__";
    2.12 + atomt t;
    2.13 + val t = (term_of o the o (parse thy)) 
    2.14 +	     "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";
    2.15 + atomt t;
    2.16 +(*andere konkrete Syntax ???*)
    2.17 +
    2.18 + val t = (term_of o the o (parse thy)) "Float ((1,2),(0,0)) * I__";
    2.19 + atomt t;
    2.20 + (*term2str t;*)
    2.21 + val t = (term_of o the o (parse thy)) 
    2.22 +	     "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
    2.23 + atomt t;
    2.24 + (*term2str t;*)
    2.25 +---------------------------------------------------------*)
    2.26 \ No newline at end of file