From c0de7a0627c9c20267a3312055ea7da683632d20 Mon Sep 17 00:00:00 2001
From: aarne <aarne@chalmers.se>
Date: Fri, 18 Dec 2009 11:08:39 +0000
Subject: mathtext examples from Bonn

---
 examples/mathtext/MathText.gf | 45 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 examples/mathtext/MathText.gf

(limited to 'examples/mathtext/MathText.gf')

diff --git a/examples/mathtext/MathText.gf b/examples/mathtext/MathText.gf
new file mode 100644
index 000000000..88357e67e
--- /dev/null
+++ b/examples/mathtext/MathText.gf
@@ -0,0 +1,45 @@
+abstract MathText = Logic ** {
+
+flags startcat = Book ;
+
+cat
+  Book ;
+  Section ;
+  [Section] {1} ;
+  Paragraph ;
+  [Paragraph] {1} ;
+  Statement ;
+  Declaration ;
+  [Declaration] {0} ;
+  Ident ;
+  Proof ;
+  Case ;
+  [Case] {2} ;
+  Number ;
+ 
+fun
+  MkBook : [Section] -> Book ;
+  
+  ParAxiom   : Ident -> Statement -> Section ;
+  ParTheorem : Ident -> Statement -> Proof -> Section ;
+
+  ParDefInd   : [Declaration] -> Ind -> Ind -> Section ;
+  ParDefPred1 : [Declaration] -> Ind -> Pred1 -> Prop -> Section ;
+  ParDefPred2 : [Declaration] -> Ind -> Pred2 -> Ind -> Prop -> Section ;
+
+  StProp : [Declaration] -> Prop -> Statement ;
+
+  DecVar  : [Var] -> Dom -> Declaration ;
+  DecProp : Prop -> Declaration ;
+
+  PrEnd  : Proof ;
+  PrStep : Statement -> Proof -> Proof ;
+  PrBy   : Ident -> Prop -> Proof -> Proof ;
+  PrCase : Number -> [Case] -> Proof ;
+  CProof : Ident -> Proof -> Case ;
+
+  IdStr  : String -> Ident ;
+
+  Two, Three, Four, Five : Number ;
+
+}
-- 
cgit v1.2.3