wneuper/isa: src/Tools/isac/IsacKnowledge/Typefix.thy@18794c7f43e2

     1 (* Title:  fixed type for _RE_parsing of strings from frontend

     2    Author: Walther Neuper

     3    9911xx

     4    (c) due to copyright terms

     5    with hints from Markus Wenzel

     6  *)

     8 theory Typefix imports "../Scripts/Script"

     9 uses ("../Scripts/scrtools.sml")

    10 ("../ME/mstools.sml") ("../ME/ctree.sml") ("../ME/ptyps.sml")

    11 ("../ME/generate.sml") ("../ME/calchead.sml") ("../ME/appl.sml")

    12 ("../ME/rewtools.sml") ("../ME/script.sml") ("../ME/solve.sml")

    13 ("../ME/inform.sml") ("../ME/mathengine.sml")

    14 ("../xmlsrc/mathml.sml") ("../xmlsrc/datatypes.sml")

    15 ("../xmlsrc/pbl-met-hierarchy.sml") ("../xmlsrc/thy-hierarchy.sml")

    16 ("../xmlsrc/interface-xml.sml") ("../FE-interface/messages.sml")

    17 ("../FE-interface/states.sml") ("../FE-interface/interface.sml")

    18 ("../print_exn_G.sml")

    19 begin

    21 syntax

    23   "_plus"  :: 'a

    24   "_minus" :: 'a

    25   "_umin"  :: 'a

    26   "_times" :: 'a

    28 translations

    30   "op +"  => "_plus  :: [real, real]  => real"  (*infixl 65    *)

    31   "op -"  => "_minus :: [real, real] => real"   (*infixl 65    *)

    32   "uminus"=> "_umin  :: [real] => real"         (*"- _" [80] 80*)

    33   "op *"  => "_times :: [real, real] => real"   (*infixl 70    *)

    35 ML {*

    36 val parse_translation =

    37     [("_plus", curry Term.list_comb (Syntax.const "op +")),

    38      ("_minus", curry Term.list_comb (Syntax.const "op -")),

    39      ("_umin", curry Term.list_comb (Syntax.const "uminus")),

    40      ("_times", curry Term.list_comb (Syntax.const "op *"))];

    41 *}

    43 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 24 Aug 2010 11:46:09 +0200
branch	isac-update-Isa09-2
changeset 37944	18794c7f43e2
parent 37943	ab57fbfcfffd
child 37945	b63c897f4977
permissions	-rw-r--r--