diff --git a/examples/logic/LexTheory.gf b/examples/logic/LexTheory.gf
new file mode 100644
index 000000000..8bdd715a0
--- /dev/null
+++ b/examples/logic/LexTheory.gf
@@ -0,0 +1,8 @@
+interface LexTheory = open Grammar in {
+
+  oper
+    assume_VS : VS ;
+    case_N : N ;
+    have_V2 : V2 ;
+
+}
diff --git a/examples/logic/LexTheoryEng.gf b/examples/logic/LexTheoryEng.gf
new file mode 100644
index 000000000..556bd2b24
--- /dev/null
+++ b/examples/logic/LexTheoryEng.gf
@@ -0,0 +1,7 @@
+instance LexTheoryEng of LexTheory = open GrammarEng,ParadigmsEng,IrregEng in {
+  oper
+    assume_VS = mkVS (regV "assume") ;
+    case_N = regN "case" ;
+    have_V2 = dirV2 have_V ;
+
+}
diff --git a/examples/logic/Theory.gf b/examples/logic/Theory.gf
new file mode 100644
index 000000000..778e0a8ec
--- /dev/null
+++ b/examples/logic/Theory.gf
@@ -0,0 +1,47 @@
+abstract Theory = {
+
+  cat
+    Chapter ;
+    Jment ;
+    [Jment] {0} ;
+    Decl ;
+    [Decl] {0} ;
+    Prop ;
+    Proof ;
+    [Proof] {2} ;
+    Branch ;
+    Typ ;
+    Obj ;
+    Label ;
+    Ref ;
+    [Ref] ;
+    Adverb ;
+    Number ;
+    
+  fun
+    Chap       : Label -> [Jment] -> Chapter ;          -- title, text
+
+    JDefObj    : [Decl] -> Obj -> Obj -> Jment ;        -- a = b (G)
+    JDefObjTyp : [Decl] -> Typ -> Obj -> Obj -> Jment ; -- a = b : A (G)
+    JDefProp   : [Decl] -> Prop -> Prop -> Jment ;      -- A = B : Prop (G)
+    JThm       : [Decl] -> Prop -> Proof -> Jment ;     -- p : P (G)
+
+    DProp      : Prop  -> Decl ;                        -- assume P
+    DPropLabel : Label -> Prop -> Label ;               -- assume P (h)
+    DTyp       : Obj   -> Typ -> Decl ;                 -- let x,y be T
+
+    PProp      : Prop -> Proof ;                        -- P.
+    PAdvProp   : Adverb -> Prop -> Proof ;              -- Hence, P.
+    PDecl      : Decl -> Proof ;                        -- Assume P.
+    PBranch    : Branch -> [Proof] -> Proof ;           -- By cases: P1 P2
+
+    BCases     : Number -> Branch ;                     -- We have n cases.
+    
+    ARef       : Ref -> Adverb ;                        -- by Thm 2
+    AHence     : Adverb ;                               -- therefore
+    AAFort     : Adverb ;                               -- a fortiori
+
+    RLabel     : Label -> Ref ;                         -- Thm 2
+    RMany      : [Ref] -> Ref ;                         -- Thm 2 and Lemma 4
+
+}
diff --git a/examples/logic/TheoryEng.gf b/examples/logic/TheoryEng.gf
new file mode 100644
index 000000000..a45bc0fdd
--- /dev/null
+++ b/examples/logic/TheoryEng.gf
@@ -0,0 +1,10 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+concrete TheoryEng of Theory = TheoryI with
+  (LexTheory = LexTheoryEng), 
+  (Grammar = GrammarEng), 
+  (Symbolic = SymbolicEng), 
+  (Symbol = SymbolEng), 
+  (Combinators = CombinatorsEng), 
+  (Constructors = ConstructorsEng), 
+  ;
\ No newline at end of file
diff --git a/examples/logic/TheoryI.gf b/examples/logic/TheoryI.gf
new file mode 100644
index 000000000..9ab457536
--- /dev/null
+++ b/examples/logic/TheoryI.gf
@@ -0,0 +1,56 @@
+incomplete concrete TheoryI of Theory = 
+  open 
+    LexTheory,
+    Grammar, 
+    Symbolic, 
+    Symbol,
+    Combinators, 
+    Constructors, 
+    (C=ConstructX),
+    Prelude 
+  in {
+
+lincat
+  Chapter = Text ;
+  Jment   = Text ;
+  Decl    = Text ;
+  Prop    = S ;
+  Branch  = S ;
+  Proof   = Text ;
+  [Proof] = Text ;
+  Typ     = CN ;
+  Obj     = NP ;
+  Label   = NP ;
+  Adverb  = PConj ;
+  Ref     = NP ;
+  [Ref]   = [NP] ;
+  Number  = Num ;
+
+lin
+  Chap title jments = 
+    appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
+
+  JDefObj decl a b = 
+    appendText decl (mkUtt (mkS (pred b a))) ;
+
+  DProp p = 
+    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
+  DTyp a ty = --- x pro a: refresh bug
+    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
+
+  PProp p = mkText (mkPhr p) TEmpty ;
+  PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
+  PDecl d = d ;
+  PBranch b ps = mkText (mkPhr b) ps ;
+
+  BCases n = 
+    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ;
+
+  ARef h = mkAdv by8means_Prep h ;
+  AHence = therefore_PConj ;
+  AAFort = C.mkPConj ["a fortiori"] ;
+
+  RLabel h = h ;
+  RMany rs = mkNP and_Conj rs ;
+
+}
diff --git a/lib/resource-1.0/Makefile b/lib/resource-1.0/Makefile
index 5a90dff09..cd6b1fa90 100644
--- a/lib/resource-1.0/Makefile
+++ b/lib/resource-1.0/Makefile
@@ -58,7 +58,14 @@ present:
 	mv */*.gfc */*.gfr ../present
 
 mathematical:
-	$(GF) -make -nocf $(GFCP) mathematical/Mathematical???.gf
+	$(GFCC) mathematical/MathematicalEng.gf
+	$(GFCC) mathematical/MathematicalNor.gf
+	$(GFCC) mathematical/MathematicalGer.gf
+	$(GFCC) mathematical/MathematicalSpa.gf
+	$(GFCC) mathematical/MathematicalIta.gf
+	$(GFCC) mathematical/MathematicalFre.gf
+	$(GFCC) mathematical/MathematicalSwe.gf
+	$(GFCC) mathematical/MathematicalFin.gf
 	mv mathematical/*.gfc ../mathematical
 
 multimodal:
diff --git a/lib/resource-1.0/api/Combinators.gf b/lib/resource-1.0/api/Combinators.gf
index eaeec71bf..4cb19d93a 100644
--- a/lib/resource-1.0/api/Combinators.gf
+++ b/lib/resource-1.0/api/Combinators.gf
@@ -20,7 +20,10 @@ incomplete resource Combinators = open Grammar in {
                                        = \a,x,y -> PredVP (ConjNP and_Conj (BaseNP x y)) (UseComp (CompAP (PositA a))) ;
       pred : N -> NP -> Cl
                                        = \n,x -> PredVP x (UseComp (CompNP (DetCN (DetSg (SgQuant IndefArt) NoOrd) (UseN n)))) ;
-      pred : N2 -> NP -> NP -> Cl 
+      pred : CN -> NP -> Cl
+                                       = \n,x -> PredVP x (UseComp (CompNP (DetCN (DetSg (SgQuant IndefArt) NoOrd) n))) ;
+      pred : NP -> NP -> Cl
+                                       = \n,x -> PredVP x (UseComp (CompNP n)) ;      pred : N2 -> NP -> NP -> Cl 
                                        = \n,x,y -> PredVP x (UseComp (CompNP (DetCN (DetSg (SgQuant IndefArt) NoOrd) (ComplN2 n y)))) ;
       pred : N -> NP -> NP -> Cl 
                                        = \n,x,y -> PredVP (ConjNP and_Conj (BaseNP x y)) (UseComp (CompNP (DetCN (DetPl (PlQuant IndefArt) NoNum NoOrd) (UseN n)))) ;
@@ -97,5 +100,9 @@ incomplete resource Combinators = open Grammar in {
 
       } ;
 
+-- This is not in ground API, because it would destroy parsing.
+
+    appendText : Text -> Text -> Text 
+                = \x,y -> {s = x.s ++ y.s ; lock_Text = <>} ;
 
 }
diff --git a/lib/resource-1.0/api/Constructors.gf b/lib/resource-1.0/api/Constructors.gf
index f6547f148..e5b5f35d1 100644
--- a/lib/resource-1.0/api/Constructors.gf
+++ b/lib/resource-1.0/api/Constructors.gf
@@ -38,7 +38,7 @@ incomplete resource Constructors = open Grammar in {
 
     mkText : overload {
       mkText : Text               ;   -- [empty text]
-      mkText : Phr -> Text -> Text;   -- John walks. ...
+      mkText : Phr -> Text -> Text    -- John walks. ...
       } ;
 
     mkPhr : overload {