From e89fdae2fa1626348d8025824a7469252fa85e42 Mon Sep 17 00:00:00 2001
From: aarne <aarne@chalmers.se>
Date: Mon, 22 Jun 2009 15:39:08 +0000
Subject: next-lib renamed to lib, lib to old-lib

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

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

diff --git a/next-lib/src/prelude/Latex.gf b/next-lib/src/prelude/Latex.gf
deleted file mode 100644
index 2fd2f9ec8..000000000
--- a/next-lib/src/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