Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Pure/isac/IsacKnowledge/Typefix.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 21 Jul 2010 13:53:39 +0200
branchisac-from-Isabelle2009-2
changeset 37871 875b6efa7ced
permissions -rw-r--r--
added isac-hook in Pure/thm and isac-code 
     1 (* fixed type for _RE_parsing of strings from frontend 

     2    WN.11.99, from Markus Wenzel

     3  *)

     4 

     5 Typefix = Script +

     6 

     7 syntax

     8        

     9   "_plus"  :: 'a

    10   "_minus" :: 'a

    11   "_umin"  :: 'a

    12   "_times" :: 'a

    13 

    14 translations

    15 

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

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

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

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

    20 

    21 end

    22 

    23 

    24 ML

    25 

    26 val parse_translation = 

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

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

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

    30      ("_times", curry Term.list_comb (Syntax.const "op *"))];
wneuper/isa