1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Trig.thy	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,4 @@
     1.4 +
     1.5 +Trig = 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/Typefix.thy	Thu Apr 17 18:01:03 2003 +0200
     2.3 @@ -0,0 +1,30 @@
     2.4 +(* fixed type for _RE_parsing of strings from frontend 
     2.5 +   WN.11.99, from Markus Wenzel
     2.6 + *)
     2.7 +
     2.8 +Typefix = Script +
     2.9 +
    2.10 +syntax
    2.11 +       
    2.12 +  "_plus"  :: 'a
    2.13 +  "_minus" :: 'a
    2.14 +  "_umin"  :: 'a
    2.15 +  "_times" :: 'a
    2.16 +
    2.17 +translations
    2.18 +
    2.19 +  "op +"  => "_plus  :: [real, real]  => real"  (*infixl 65    *)
    2.20 +  "op -"  => "_minus :: [real, real] => real"   (*infixl 65    *)
    2.21 +  "uminus"=> "_umin  :: [real] => real"         (*"- _" [80] 80*)
    2.22 +  "op *"  => "_times :: [real, real] => real"   (*infixl 70    *)
    2.23 +
    2.24 +end
    2.25 +
    2.26 +
    2.27 +ML
    2.28 +
    2.29 +val parse_translation = 
    2.30 +    [("_plus", curry Term.list_comb (Syntax.const "op +")),  
    2.31 +     ("_minus", curry Term.list_comb (Syntax.const "op -")), 
    2.32 +     ("_umin", curry Term.list_comb (Syntax.const "uminus")),
    2.33 +     ("_times", curry Term.list_comb (Syntax.const "op *"))];

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/sml/IsacKnowledge/Vect.thy	Thu Apr 17 18:01:03 2003 +0200
     3.3 @@ -0,0 +1,5 @@
     3.4 +Vect = Real +
     3.5 +(*-------------------- consts ------------------------------------------------*)
     3.6 +
     3.7 +(*-------------------- rules -------------------------------------------------*)
     3.8 +end