markup

2 files changed, 6 insertions, 3 deletions

diff --git a/grammars/logic/ArithmEng.gf b/grammars/logic/ArithmEng.gf
index 8c78132ea..e09f14396 100644
--- a/grammars/logic/ArithmEng.gf
+++ b/grammars/logic/ArithmEng.gf
@@ -1,3 +1,5 @@
+--# -path=.:../prelude
+
 concrete ArithmEng of Arithm = LogicEng ** open LogicResEng in {
 
 lin
diff --git a/grammars/logic/LogicEng.gf b/grammars/logic/LogicEng.gf
index 3b823fcb0..b708068e2 100644
--- a/grammars/logic/LogicEng.gf
+++ b/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} ;