1.1 --- a/src/Tools/isac/IsacKnowledge/Typefix.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,68 +0,0 @@
     1.4 -(* Title:  fixed type for _RE_parsing of strings from frontend 
     1.5 -   Author: Walther Neuper
     1.6 -   9911xx 
     1.7 -   (c) due to copyright terms
     1.8 -   with hints from Markus Wenzel
     1.9 - *)
    1.10 -
    1.11 -theory Typefix imports "../Scripts/Script"
    1.12 -uses ("../Scripts/scrtools.sml") 
    1.13 -("../ME/mstools.sml") ("../ME/ctree.sml") ("../ME/ptyps.sml")
    1.14 -("../ME/generate.sml") ("../ME/calchead.sml") ("../ME/appl.sml")
    1.15 -("../ME/rewtools.sml") ("../ME/script.sml") ("../ME/solve.sml")
    1.16 -("../ME/inform.sml") ("../ME/mathengine.sml")
    1.17 -("../xmlsrc/mathml.sml") ("../xmlsrc/datatypes.sml")
    1.18 -("../xmlsrc/pbl-met-hierarchy.sml") ("../xmlsrc/thy-hierarchy.sml")
    1.19 -("../xmlsrc/interface-xml.sml") ("../FE-interface/messages.sml")
    1.20 -("../FE-interface/states.sml") ("../FE-interface/interface.sml")
    1.21 -("../print_exn_G.sml")
    1.22 -begin
    1.23 -use "../Scripts/scrtools.sml"
    1.24 -
    1.25 -use "../ME/mstools.sml"
    1.26 -use "../ME/ctree.sml"
    1.27 -use "../ME/ptyps.sml"
    1.28 -use "../ME/generate.sml"
    1.29 -use "../ME/calchead.sml"
    1.30 -use "../ME/appl.sml"
    1.31 -use "../ME/rewtools.sml"
    1.32 -use "../ME/script.sml"
    1.33 -use "../ME/solve.sml"
    1.34 -use "../ME/inform.sml"
    1.35 -use "../ME/mathengine.sml"
    1.36 -
    1.37 -use "../xmlsrc/mathml.sml"
    1.38 -use "../xmlsrc/datatypes.sml"
    1.39 -use "../xmlsrc/pbl-met-hierarchy.sml"
    1.40 -use "../xmlsrc/thy-hierarchy.sml" 
    1.41 -use "../xmlsrc/interface-xml.sml"
    1.42 -
    1.43 -use "../FE-interface/messages.sml"
    1.44 -use "../FE-interface/states.sml"
    1.45 -use "../FE-interface/interface.sml"
    1.46 -
    1.47 -use "../print_exn_G.sml"
    1.48 -
    1.49 -syntax
    1.50 -       
    1.51 -  "_plus"  :: 'a
    1.52 -  "_minus" :: 'a
    1.53 -  "_umin"  :: 'a
    1.54 -  "_times" :: 'a
    1.55 -
    1.56 -translations
    1.57 -
    1.58 -  "op +"  => "_plus  :: [real, real]  => real"  (*infixl 65    *)
    1.59 -  "op -"  => "_minus :: [real, real] => real"   (*infixl 65    *)
    1.60 -  "uminus"=> "_umin  :: [real] => real"         (*"- _" [80] 80*)
    1.61 -  "op *"  => "_times :: [real, real] => real"   (*infixl 70    *)
    1.62 -
    1.63 -ML {*
    1.64 -val parse_translation = 
    1.65 -    [("_plus", curry Term.list_comb (Syntax.const "op +")),  
    1.66 -     ("_minus", curry Term.list_comb (Syntax.const "op -")), 
    1.67 -     ("_umin", curry Term.list_comb (Syntax.const "uminus")),
    1.68 -     ("_times", curry Term.list_comb (Syntax.const "op *"))];
    1.69 -*}
    1.70 -
    1.71 -end
    1.72 \ No newline at end of file