From c8ceed08efcc0bdc1fcbd89bce643d9f52f0991b Mon Sep 17 00:00:00 2001
From: aarne <aarne@chalmers.se>
Date: Wed, 9 Dec 2009 09:47:16 +0000
Subject: moving a few things to deprecated

---
 old-lib/prelude/Latex.gf | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 old-lib/prelude/Latex.gf

(limited to 'old-lib/prelude/Latex.gf')

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 ;
-}
-    
-
-- 
cgit v1.2.3