markup

grammars/logic/ArithmEng.gf

@@ -1,3 +1,5 @@
+--# -path=.:../prelude
+
 concrete ArithmEng of Arithm = LogicEng ** open LogicResEng in {
 
 lin

grammars/logic/LogicEng.gf

@@ -1,4 +1,4 @@
-concrete LogicEng of Logic = open LogicResEng in {
+concrete LogicEng of Logic = open LogicResEng, Prelude in {
 
 flags lexer=vars ; unlexer=text ;
 
@@ -8,9 +8,10 @@ lincat
 
 lin 
 Statement A = {s = A.s ++ "."} ;
-ThmWithProof A a = {s = ["Theorem ."] ++ A.s ++ [". <p> Proof ."] ++ a.s ++ "."} ;
+ThmWithProof A a = {s = 
+  ["Theorem ."] ++ A.s ++ "." ++ PARA ++ "Proof" ++ "." ++ a.s ++ "."} ;
 ThmWithTrivialProof A a = 
-  {s = "Theorem" ++ "." ++ A.s ++ [". <p> Proof . Trivial ."]} ;
+  {s = "Theorem" ++ "." ++ A.s ++ "." ++ PARA ++ "Proof" ++ "." ++ "Trivial" ++ "."} ;
 Disj A B = {s = A.s ++ "or" ++ B.s} ;
 Conj A B = {s = A.s ++ "and" ++ B.s} ;
 Impl A B = {s = "if" ++ A.s ++ "then" ++ B.s} ;

grammars/prelude/Prelude.gf

@@ -94,6 +94,7 @@ oper
     glueOpt : Str -> Str -> Str = \x,y -> variants {glue x y ; x ++ y} ;
     noglueOpt : Str -> Str -> Str = \x,y -> variants {x ++ y ; glue x y} ;
 
--- this should be hidden, and never changed since it's hardcoded in (un)lexers
+-- these should be hidden, and never changed since it's hardcoded in (un)lexers
     BIND : Str = "&+" ;
+    PARA : Str = "&-" ;
 } ;