diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/IsacKnowledge/Typefix.thy
--- a/src/Tools/isac/IsacKnowledge/Typefix.thy	Wed Aug 25 15:15:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(* Title:  fixed type for _RE_parsing of strings from frontend 
-   Author: Walther Neuper
-   9911xx 
-   (c) due to copyright terms
-   with hints from Markus Wenzel
- *)
-
-theory Typefix imports "../Scripts/Script"
-uses ("../Scripts/scrtools.sml") 
-("../ME/mstools.sml") ("../ME/ctree.sml") ("../ME/ptyps.sml")
-("../ME/generate.sml") ("../ME/calchead.sml") ("../ME/appl.sml")
-("../ME/rewtools.sml") ("../ME/script.sml") ("../ME/solve.sml")
-("../ME/inform.sml") ("../ME/mathengine.sml")
-("../xmlsrc/mathml.sml") ("../xmlsrc/datatypes.sml")
-("../xmlsrc/pbl-met-hierarchy.sml") ("../xmlsrc/thy-hierarchy.sml")
-("../xmlsrc/interface-xml.sml") ("../FE-interface/messages.sml")
-("../FE-interface/states.sml") ("../FE-interface/interface.sml")
-("../print_exn_G.sml")
-begin
-use "../Scripts/scrtools.sml"
-
-use "../ME/mstools.sml"
-use "../ME/ctree.sml"
-use "../ME/ptyps.sml"
-use "../ME/generate.sml"
-use "../ME/calchead.sml"
-use "../ME/appl.sml"
-use "../ME/rewtools.sml"
-use "../ME/script.sml"
-use "../ME/solve.sml"
-use "../ME/inform.sml"
-use "../ME/mathengine.sml"
-
-use "../xmlsrc/mathml.sml"
-use "../xmlsrc/datatypes.sml"
-use "../xmlsrc/pbl-met-hierarchy.sml"
-use "../xmlsrc/thy-hierarchy.sml" 
-use "../xmlsrc/interface-xml.sml"
-
-use "../FE-interface/messages.sml"
-use "../FE-interface/states.sml"
-use "../FE-interface/interface.sml"
-
-use "../print_exn_G.sml"
-
-syntax
-       
-  "_plus"  :: 'a
-  "_minus" :: 'a
-  "_umin"  :: 'a
-  "_times" :: 'a
-
-translations
-
-  "op +"  => "_plus  :: [real, real]  => real"  (*infixl 65    *)
-  "op -"  => "_minus :: [real, real] => real"   (*infixl 65    *)
-  "uminus"=> "_umin  :: [real] => real"         (*"- _" [80] 80*)
-  "op *"  => "_times :: [real, real] => real"   (*infixl 70    *)
-
-ML {*
-val parse_translation = 
-    [("_plus", curry Term.list_comb (Syntax.const "op +")),  
-     ("_minus", curry Term.list_comb (Syntax.const "op -")), 
-     ("_umin", curry Term.list_comb (Syntax.const "uminus")),
-     ("_times", curry Term.list_comb (Syntax.const "op *"))];
-*}
-
-end
\ No newline at end of file