moving a few things to deprecated

1 files changed, 0 insertions, 12 deletions

diff --git a/old-lib/prelude/Latex.gf b/old-lib/prelude/Latex.gf
deleted file mode 100644
index 2fd2f9ec8..000000000
--- a/old-lib/prelude/Latex.gf
+++ /dev/null
@@ -1,12 +0,0 @@
-resource Latex = open Prelude in {
-  oper
-    command : Str -> Str = \c -> "\\" + c ;
-    fun1 : Str -> Str -> Str = \f,x -> "\\" + f + "{" ++ x ++ "}" ;    
-    fun2 : Str -> Str -> Str -> Str = 
-      \f,x,y -> "\\" + f + "{" ++ x ++ "}{" ++ y ++ "}" ;
-    begin : Str -> Str = \e -> "\\begin{" + e + "}" ;   
-    end : Str -> Str = \e -> "\\end{" + e + "}" ;
-    inEnv : Str -> Str -> Str = \e,s -> begin e ++ s ++ end e ;
-}
-    
-