1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Typefix.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,32 @@
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 "../ProgLang/Script" begin
1.12 +
1.13 +syntax
1.14 +
1.15 + "_plus" :: 'a
1.16 + "_minus" :: 'a
1.17 + "_umin" :: 'a
1.18 + "_times" :: 'a
1.19 +
1.20 +translations
1.21 +
1.22 + "op +" => "_plus :: [real, real] => real" (*infixl 65 *)
1.23 + "op -" => "_minus :: [real, real] => real" (*infixl 65 *)
1.24 + "uminus"=> "_umin :: [real] => real" (*"- _" [80] 80*)
1.25 + "op *" => "_times :: [real, real] => real" (*infixl 70 *)
1.26 +
1.27 +ML {*
1.28 +val parse_translation =
1.29 + [("_plus", curry Term.list_comb (Syntax.const "op +")),
1.30 + ("_minus", curry Term.list_comb (Syntax.const "op -")),
1.31 + ("_umin", curry Term.list_comb (Syntax.const "uminus")),
1.32 + ("_times", curry Term.list_comb (Syntax.const "op *"))];
1.33 +*}
1.34 +
1.35 +end
1.36 \ No newline at end of file