From be0e4d6203b96072a5a700af78039e8cfeea5651 Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Fri, 16 Jun 2006 08:06:52 +0000
Subject: [PATCH] tutorial example of LF

---
 doc/tutorial/gf-tutorial2.txt | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/doc/tutorial/gf-tutorial2.txt b/doc/tutorial/gf-tutorial2.txt
index 978d46f36..31622a62b 100644
--- a/doc/tutorial/gf-tutorial2.txt
+++ b/doc/tutorial/gf-tutorial2.txt
@@ -1876,15 +1876,19 @@ In a logical framework, the formalization of a mathematical theory
 is a set of type and function declarations. The following is an example
 of such a theory, represented as an ``abstract`` module in GF.
 ```
-  abstract Geometry = {
-    cat 
-      Line ; Point ; Circle ;            -- basic types of figures
-      Prop ;                             -- proposition
-    fun
-      Parallel : Line -> Line -> Prop ;  -- x is parallel to y
-      Centre : Circle -> Point ;         -- the centre of c
+abstract Arithm = {
+  cat
+    Prop ;    -- proposition
+    Nat ;     -- natural number
+  fun
+    Zero : Nat ;                  -- 0
+    Succ : Nat -> Nat ;           -- successor of x
+    Even : Nat -> Prop ;          -- x is even
+    And  : Prop -> Prop -> Prop ; -- A and B
     } 
 ```
+A concrete syntax is given below, as an example of using the resource grammar
+library.