diff --git a/regression/modulebad10/functor.slf b/regression/modulebad10/functor.slf
new file mode 100644
index 00000000..7009abd0
--- /dev/null
+++ b/regression/modulebad10/functor.slf
@@ -0,0 +1,18 @@
+package regression.modulebad10
+
+module functor
+
+requires
+
+abstract syntax e
+
+judgment eq: e = e
+
+  --- eq-refl
+  e = e
+
+provides
+
+terminals nil
+
+syntax l ::= nil | e, l
diff --git a/regression/modulebad10/test.slf b/regression/modulebad10/test.slf
new file mode 100644
index 00000000..4e00ea22
--- /dev/null
+++ b/regression/modulebad10/test.slf
@@ -0,0 +1,14 @@
+package regression.modulebad10
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+judgment nat-eq: n = n
+
+  --- nat-refl
+  n = n
+
+module m = regression.modulebad10.functor[n, nat-eq] //!
diff --git a/regression/modulebad11/nats.slf b/regression/modulebad11/nats.slf
new file mode 100644
index 00000000..46bfb1bf
--- /dev/null
+++ b/regression/modulebad11/nats.slf
@@ -0,0 +1,8 @@
+package regression.modulebad11
+
+module nats provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
diff --git a/regression/modulebad11/test.slf b/regression/modulebad11/test.slf
new file mode 100644
index 00000000..5a69dcbd
--- /dev/null
+++ b/regression/modulebad11/test.slf
@@ -0,0 +1,10 @@
+package regression.modulebad11
+
+module test
+
+requires
+
+syntax n = regression.modulebad11.nats.n //! should be in 'imports' section, not 'requires'
+
+provides
+
diff --git a/regression/modulegood05/test.slf b/regression/modulegood05/test.slf
index d2104b6c..a14942d2 100644
--- a/regression/modulegood05/test.slf
+++ b/regression/modulegood05/test.slf
@@ -82,12 +82,11 @@ end theorem
 
 module boolbt = regression.modulegood05.foldablebt
 [
-  boolid, 
-  boolnonid, 
-  b, 
-  lor, 
-  lor-left-id, 
-  lor-right-id, 
+  boolid,
+  boolnonid,
+  lor,
+  lor-left-id,
+  lor-right-id,
   lor-commutative
 ]
 
diff --git a/regression/modulegood06/test.slf b/regression/modulegood06/test.slf
index 4cce86de..e0fb896a 100644
--- a/regression/modulegood06/test.slf
+++ b/regression/modulegood06/test.slf
@@ -76,7 +76,7 @@ theorem lor-total:
   proof by unproved //!
 end theorem
 
-module boolbt = regression.modulegood06.foldablebt[boolid, boolnonid, b, lor, lor-commutative, lor-associative, lor-total]
+module boolbt = regression.modulegood06.foldablebt[boolid, boolnonid, lor, lor-commutative, lor-associative, lor-total]
 
 syntax bt = boolbt.bt ::= Leaf | Node bt b bt
 
diff --git a/regression/modulegood11/functor.slf b/regression/modulegood11/functor.slf
new file mode 100644
index 00000000..d2090fc1
--- /dev/null
+++ b/regression/modulegood11/functor.slf
@@ -0,0 +1,20 @@
+package regression.modulegood11
+
+module functor
+
+requires
+
+abstract syntax e
+
+judgment eq: e = e
+
+  --- eq-refl
+  e = e
+
+provides
+
+theorem self-equal:
+  forall e1
+  exists e1 = e1
+  proof by rule eq-refl
+end theorem
diff --git a/regression/modulegood11/test.slf b/regression/modulegood11/test.slf
new file mode 100644
index 00000000..e98076d8
--- /dev/null
+++ b/regression/modulegood11/test.slf
@@ -0,0 +1,17 @@
+package regression.modulegood11
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+module m = regression.modulegood11.functor[n]
+
+judgment n-eq = m.eq : n = n
+
+theorem nat-self-equal:
+  forall n1
+  exists n1 = n1
+  proof by rule m.eq-refl
+end theorem
diff --git a/regression/modulegood12/functor.slf b/regression/modulegood12/functor.slf
new file mode 100644
index 00000000..1271550b
--- /dev/null
+++ b/regression/modulegood12/functor.slf
@@ -0,0 +1,18 @@
+package regression.modulegood12
+
+module functor
+
+imports
+  syntax n = regression.modulegood12.nats.n
+
+requires
+  abstract syntax e
+
+provides
+
+terminals wrap
+
+syntax w ::= wrap e
+
+judgment wrap-n: w = n
+
diff --git a/regression/modulegood12/nats.slf b/regression/modulegood12/nats.slf
new file mode 100644
index 00000000..27e0acc2
--- /dev/null
+++ b/regression/modulegood12/nats.slf
@@ -0,0 +1,13 @@
+package regression.modulegood12
+
+module nats provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+judgment equal: n = n
+
+  --- eq-refl
+  n = n
+
diff --git a/regression/modulegood12/test.slf b/regression/modulegood12/test.slf
new file mode 100644
index 00000000..5d54dba4
--- /dev/null
+++ b/regression/modulegood12/test.slf
@@ -0,0 +1,12 @@
+package regression.modulegood12
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+module m = regression.modulegood12.functor[n]
+
+syntax mw = m.w
+
diff --git a/regression/test1/set.slf b/regression/test1/set.slf
index 0a88a3bf..db4e44f8 100644
--- a/regression/test1/set.slf
+++ b/regression/test1/set.slf
@@ -28,7 +28,7 @@ provides
 
 terminals in notin ok
 
-module repm = regression.test1.list[e,elem-eq]
+module repm = regression.test1.list[e]
 
 syntax r = repm.l
   ::= 0
diff --git a/regression/test1/test.slf b/regression/test1/test.slf
index 212ca03d..12fd25f9 100644
--- a/regression/test1/test.slf
+++ b/regression/test1/test.slf
@@ -7,7 +7,7 @@ module nat = org.sasylf.util.Natural
 syntax n = nat.n
 
 module setb =
-regression.test1.set[n,nat.equal,nat.notequal,nat.ne-anti-reflexive,nat.eq-or-ne]
+regression.test1.set[n,nat.notequal,nat.ne-anti-reflexive,nat.eq-or-ne]
 
 terminals in
 
diff --git a/src/edu/cmu/cs/sasylf/ast/CompUnit.java b/src/edu/cmu/cs/sasylf/ast/CompUnit.java
index c0b3ec86..0bb9e8d6 100644
--- a/src/edu/cmu/cs/sasylf/ast/CompUnit.java
+++ b/src/edu/cmu/cs/sasylf/ast/CompUnit.java
@@ -25,6 +25,7 @@
 public class CompUnit extends Node implements Module {
 	private PackageDeclaration packageDecl;
 	private String moduleName;
+	private List<Part> imports = new ArrayList<Part>();
 	private List<Part> params = new ArrayList<Part>();
 	private List<Part> parts = new ArrayList<Part>();
 	private int parseReports;
@@ -43,6 +44,15 @@ protected void updateReportCount() {
 		parseReports = ErrorHandler.getReports().size();
 	}
 
+	/**
+	 * Add an import chunk to this compilation unit.
+	 * @param c part to add, must not be null
+	 */
+	public void addImportChunk(Part c) {
+		imports.add(c);
+		updateReportCount();
+	}
+
 	/**
 	 * Add a chunk that is required by this module.
 	 * @param c part to add, must not be null
@@ -85,6 +95,13 @@ public void prettyPrint(PrintWriter out) {
 			out.println("module " + moduleName);
 		}
 
+		if (!imports.isEmpty()) {
+			out.println("imports");
+			for (Part part : imports) {
+				part.prettyPrint(out);
+			}
+		}
+
 		if (!params.isEmpty()) {
 			out.println("requires");
 			for (Part part : params) {
@@ -141,14 +158,30 @@ public boolean typecheck(ModuleFinder mf, ModuleId id) {
 	public void typecheck(Context ctx, ModuleId id) {
 
 		if (id != null) checkFilename(id);
-		for (Part part : params) {
+		// Process imports first — they are external dependencies with no args needed
+		for (Part part : imports) {
 			try {
 				part.typecheck(ctx);
-				if (part instanceof JudgmentPart) {
+			} catch (SASyLFError ex) {
+				// already reported
+			}
+		}
+		for (Part part : params) {
+			try {
+				// Check for import-style (rename) declarations in requires — they belong in imports
+				if (part instanceof SyntaxPart) {
+					for (Syntax s : ((SyntaxPart) part).getSyntax()) {
+						if (s instanceof RenameSyntaxDeclaration) {
+							ErrorHandler.recoverableError(Errors.IMPORT_IN_REQUIRES, s);
+						}
+					}
+				} else if (part instanceof JudgmentPart) {
 					List<Node> pieces = new ArrayList<>();
 					part.collectTopLevel(pieces);
 					for (Node n : pieces) {
-						if (n instanceof Judgment) {
+						if (n instanceof RenameJudgment) {
+							ErrorHandler.recoverableError(Errors.IMPORT_IN_REQUIRES, (Node)n);
+						} else if (n instanceof Judgment) {
 							Judgment j = (Judgment)n;
 							if (!j.isAbstract() && j.getRules().isEmpty()) {
 								ErrorHandler.recoverableError(Errors.ABSTRACT_REQUIRED, j);
@@ -156,6 +189,7 @@ public void typecheck(Context ctx, ModuleId id) {
 						}
 					}
 				}
+				part.typecheck(ctx);
 			} catch (SASyLFError ex) {
 				// already reported
 			}
@@ -189,6 +223,9 @@ private void checkFilename(ModuleId id) {
 	 */
 	@Override
 	public void collectTopLevel(Collection<? super Node> things) {
+		for (Part part : imports) {
+			part.collectTopLevel(things);
+		}
 		for (Part part : params) {
 			part.collectTopLevel(things);
 		}
@@ -202,6 +239,9 @@ public void collectTopLevel(Collection<? super Node> things) {
 	 */
 	@Override
 	public void collectRuleLike(Map<String,? super RuleLike> map) {
+		for (Part part : imports) {
+			part.collectRuleLike(map);
+		}
 		for (Part part : params) {
 			part.collectRuleLike(map);
 		}
@@ -216,10 +256,12 @@ public void collectRuleLike(Map<String,? super RuleLike> map) {
 	 */
 	@Override
 	public void collectQualNames(Consumer<QualName> consumer) {
+		for (Part part : imports) {
+			part.collectQualNames(consumer);
+		}
 		for (Part part : params) {
 			part.collectQualNames(consumer);
 		}
-		
 		for (Part part : parts) {
 			part.collectQualNames(consumer);
 		}
@@ -258,14 +300,9 @@ public Object getDeclaration(Context ctx, String name) {
 
 	@Override
 	public void substitute(SubstitutionData sd) {
-		/*
-			Substitute in the following attributes:
-
-			private List<Part> params
-			private List<Part> parts
-		*/
 		if (sd.didSubstituteFor(this)) return;
 		sd.setSubstitutedFor(this);
+		// imports use external cached objects — do not substitute inside them
 		for (Part part : parts) {
 			part.substitute(sd);
 		}
@@ -285,6 +322,9 @@ public CompUnit clone() {
 	
 		clone.packageDecl = packageDecl.copy(cd);
 
+		// imports reference external cached objects — shallow copy only
+		clone.imports = new ArrayList<>(imports);
+
 		List<Part> newParams = new ArrayList<>();
 		for (Part p: params) {
 			newParams.add(p.copy(cd));
@@ -341,6 +381,10 @@ public Optional<CompUnit> accept(List<ModuleComponent> args, ModulePart mp, Cont
 			param.collectTopLevelAsModuleComponents(moduleParams);
 		});
 
+		// Only abstract components require explicit arguments;
+		// non-abstract components are included in the instantiated module automatically.
+		moduleParams.removeIf(mc -> !mc.isAbstract());
+
 		int numParams = moduleParams.size();
 		int numArgs = args.size();
 
@@ -377,6 +421,23 @@ private boolean doApplication(List<ModuleComponent> args, ModulePart mp, List<Mo
 		Map<Syntax, Syntax> paramToArgSyntax = new IdentityHashMap<Syntax, Syntax>();
 		Map<Judgment, Judgment> paramToArgJudgment = new IdentityHashMap<Judgment, Judgment>();
 
+		// Collect non-abstract syntax objects before moving (needed for derived substitution later)
+		List<Syntax> nonAbstractSyntaxes = new ArrayList<>();
+		for (Part p : this.params) {
+			if (p instanceof SyntaxPart) {
+				for (Syntax s : ((SyntaxPart) p).getSyntax()) {
+					if (!s.isAbstract()) {
+						nonAbstractSyntaxes.add(s);
+					}
+				}
+			}
+		}
+
+		// Move non-abstract Parts from requires (params) to provides (body) so they
+		// are included in the instantiated module and receive abstract-param substitutions
+		List<Part> nonAbstractParts = extractNonAbstractParts(this.params);
+		this.parts.addAll(0, nonAbstractParts);
+
 		this.params.clear();
 
 		for (int i = 0; i < args.size(); i++) {
@@ -395,11 +456,66 @@ private boolean doApplication(List<ModuleComponent> args, ModulePart mp, List<Mo
 			}
 
 		}
-		
+
+		// Apply derived substitutions for non-abstract syntax types that were implicitly
+		// mapped through abstract judgment form structure checking.
+		// For example, if abstract judgment "add: e + e = e" is matched against concrete
+		// "lor: b \/ b = b", the form check records e->b. We apply that substitution
+		// so the non-abstract syntax e (now in body) and all references to it use b.
+		for (Syntax nonAbstractSyntax : nonAbstractSyntaxes) {
+			String syntaxName = nonAbstractSyntax.getName();
+			for (Map.Entry<Syntax, Syntax> entry : paramToArgSyntax.entrySet()) {
+				if (!entry.getKey().isAbstract() && entry.getKey().getName().equals(syntaxName)) {
+					Syntax argSyntax = entry.getValue();
+					SubstitutionData derivedSd = new SubstitutionData(
+						syntaxName,
+						argSyntax.getName(),
+						argSyntax.getOriginalDeclaration(),
+						nonAbstractSyntax.getOriginalDeclaration()
+					);
+					this.substitute(derivedSd);
+					break;
+				}
+			}
+		}
+
 		this.moduleName = moduleName;
 
 		return true;
-	
+
+	}
+
+	/**
+	 * Extract all Parts containing non-abstract components from the given list of param Parts.
+	 * Creates new Part objects containing only the non-abstract components of each Part.
+	 * These Parts should be moved to the module body so they are included in the instantiation.
+	 * @param paramParts the list of Parts from the requires section
+	 * @return a list of new Parts containing only non-abstract components
+	 */
+	private List<Part> extractNonAbstractParts(List<Part> paramParts) {
+		List<Part> result = new ArrayList<>();
+		for (Part p : paramParts) {
+			if (p instanceof SyntaxPart) {
+				List<Syntax> nonAbstract = new ArrayList<>();
+				for (Syntax s : ((SyntaxPart) p).getSyntax()) {
+					if (!s.isAbstract()) nonAbstract.add(s);
+				}
+				if (!nonAbstract.isEmpty()) result.add(new SyntaxPart(nonAbstract));
+			} else if (p instanceof JudgmentPart) {
+				List<Judgment> nonAbstract = new ArrayList<>();
+				for (Judgment j : ((JudgmentPart) p).judgments) {
+					if (!j.isAbstract()) nonAbstract.add(j);
+				}
+				if (!nonAbstract.isEmpty()) result.add(new JudgmentPart(nonAbstract));
+			} else if (p instanceof TheoremPart) {
+				List<Theorem> nonAbstract = new ArrayList<>();
+				for (Theorem t : ((TheoremPart) p).getTheorems()) {
+					if (!t.isAbstract()) nonAbstract.add(t);
+				}
+				if (!nonAbstract.isEmpty()) result.add(new TheoremPart(nonAbstract));
+			}
+		}
+		return result;
 	}
 
 }
diff --git a/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java b/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java
index c4da53eb..0bb785ef 100644
--- a/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java
+++ b/src/edu/cmu/cs/sasylf/ast/ModuleComponent.java
@@ -55,4 +55,14 @@ public Optional<SubstitutionData> matchesParam(
    */
   public ModuleComponent copy(CopyData cd);
 
+  /**
+   * Returns whether this module component is abstract (i.e., requires an explicit argument
+   * during module instantiation).
+   * <br/><br/>
+   * Non-abstract components (those with concrete definitions) are automatically included
+   * in the instantiated module without requiring an explicit argument.
+   * @return true if this component is abstract, false otherwise
+   */
+  public boolean isAbstract();
+
 }
\ No newline at end of file
diff --git a/src/edu/cmu/cs/sasylf/ast/RenameJudgment.java b/src/edu/cmu/cs/sasylf/ast/RenameJudgment.java
index 3943997a..a71f98bc 100644
--- a/src/edu/cmu/cs/sasylf/ast/RenameJudgment.java
+++ b/src/edu/cmu/cs/sasylf/ast/RenameJudgment.java
@@ -125,10 +125,8 @@ public Judgment getOriginalDeclaration() {
 	@Override
 	public void substitute(SubstitutionData sd) {
 		super.substitute(sd);
-		if (sd.didSubstituteFor(this)) return;
-		sd.setSubstitutedFor(this);
-
-		original.substitute(sd);
+		// Do NOT substitute inside original — it is an externally-cached object
+		// from another module and must not be mutated by substitution.
 	}
 
 	@Override
diff --git a/src/edu/cmu/cs/sasylf/ast/RenameSyntaxDeclaration.java b/src/edu/cmu/cs/sasylf/ast/RenameSyntaxDeclaration.java
index a032988c..bcefae59 100644
--- a/src/edu/cmu/cs/sasylf/ast/RenameSyntaxDeclaration.java
+++ b/src/edu/cmu/cs/sasylf/ast/RenameSyntaxDeclaration.java
@@ -191,7 +191,8 @@ public void substitute(SubstitutionData sd) {
 		*/
 
 		if (source != null) source.substitute(sd);
-		if (original != null) original.substitute(sd);
+		// Do NOT substitute inside original — it is an externally-cached object
+		// from another module and must not be mutated by substitution.
 
 	}
 
@@ -207,9 +208,9 @@ public RenameSyntaxDeclaration copy(CopyData cd) {
 			clone.source = clone.source.copy(cd);
 		}
 		
-		if (clone.original != null) {
-			clone.original = clone.original.copy(cd);
-		}
+		// Do NOT copy original — it is an externally-cached object and must
+		// stay as the same reference so that identity comparison works correctly
+		// during module instantiation (IdentityHashMap<Syntax,Syntax>).
 		return clone;
 	}
 
diff --git a/src/edu/cmu/cs/sasylf/ast/Sugar.java b/src/edu/cmu/cs/sasylf/ast/Sugar.java
index f38f8457..379d8634 100644
--- a/src/edu/cmu/cs/sasylf/ast/Sugar.java
+++ b/src/edu/cmu/cs/sasylf/ast/Sugar.java
@@ -46,6 +46,11 @@ public Sugar(Element lhs, Clause rhs) {
 		if (rhs != null) this.setEndLocation(rhs.getEndLocation());
 	}
 	
+	@Override
+	public boolean isAbstract() {
+		return false;
+	}
+
 	@Override
 	public void prettyPrint(PrintWriter out) {
 		sugar.prettyPrint(out);
diff --git a/src/edu/cmu/cs/sasylf/ast/Syntax.java b/src/edu/cmu/cs/sasylf/ast/Syntax.java
index 64dd5563..60885e73 100644
--- a/src/edu/cmu/cs/sasylf/ast/Syntax.java
+++ b/src/edu/cmu/cs/sasylf/ast/Syntax.java
@@ -87,6 +87,14 @@ public void checkSubordination() {}
 	 */
 	public abstract SyntaxDeclaration getOriginalDeclaration();
 
+	/**
+	 * Returns whether this syntax is abstract (has no concrete productions).
+	 * Abstract syntax requires an explicit argument during module instantiation.
+	 * @return true if this syntax is abstract, false otherwise
+	 */
+	@Override
+	public abstract boolean isAbstract();
+
 	/**
 	 * Substitute inside of this Syntax according to the given substitution data.
 	 * @param sd substitution data to use
diff --git a/src/edu/cmu/cs/sasylf/ast/SyntaxDeclaration.java b/src/edu/cmu/cs/sasylf/ast/SyntaxDeclaration.java
index e67386a5..e4983495 100644
--- a/src/edu/cmu/cs/sasylf/ast/SyntaxDeclaration.java
+++ b/src/edu/cmu/cs/sasylf/ast/SyntaxDeclaration.java
@@ -757,9 +757,13 @@ public SyntaxDeclaration copy(CopyData cd) {
 
 		clone.term = null;
 
-		clone.gnt = clone.gnt.copy(cd);
+		if (clone.gnt != null) {
+			clone.gnt = clone.gnt.copy(cd);
+		}
 
-		clone.gt = clone.gt.copy(cd);
+		if (clone.gt != null) {
+			clone.gt = clone.gt.copy(cd);
+		}
 		
 		return clone;
 	}
diff --git a/src/edu/cmu/cs/sasylf/ast/Theorem.java b/src/edu/cmu/cs/sasylf/ast/Theorem.java
index 188aa729..a91c30f6 100644
--- a/src/edu/cmu/cs/sasylf/ast/Theorem.java
+++ b/src/edu/cmu/cs/sasylf/ast/Theorem.java
@@ -50,6 +50,8 @@ public Theorem(String n, Location l, boolean abs) {
 
 	public List<Fact> getForalls() { return foralls; }
 	@Override
+	public boolean isAbstract() { return isAbstract; }
+	@Override
 	public List<Element> getPremises() {
 		List<Element> l = new ArrayList<Element>();
 		for (Fact f : foralls) {
diff --git a/src/edu/cmu/cs/sasylf/parser/parser.jj b/src/edu/cmu/cs/sasylf/parser/parser.jj
index 70e06c01..8e404290 100644
--- a/src/edu/cmu/cs/sasylf/parser/parser.jj
+++ b/src/edu/cmu/cs/sasylf/parser/parser.jj
@@ -204,6 +204,7 @@ public class DSLToolkitParser {
 			// || getToken(1).kind == OR
 			|| getToken(1).kind == EXTENDS
 			|| getToken(1).kind == USE
+			|| getToken(1).kind == IMPORTS
 			|| getToken(1).kind == REQUIRES
 			|| getToken(1).kind == PROVIDES
 			|| getToken(1).kind == INTEGER_LITERAL;
@@ -273,6 +274,7 @@ public class DSLToolkitParser {
 		   t.kind == MODULE ||
 		   t.kind == NOT ||
 		   t.kind == OR ||
+		   t.kind == IMPORTS ||
 		   t.kind == PROVIDES ||
 		   t.kind == REQUIRES ||
 		   t.kind == SUBSTITUTION ||
@@ -410,6 +412,7 @@ TOKEN :
 | < CONTRADICTION: "contradiction" >
 | < USE: "use" >
 | < MODULE: "module" >
+| < IMPORTS: "imports" >
 | < REQUIRES: "requires" >
 | < PROVIDES: "provides" >
 | < EXTENDS: "extends" >
@@ -1552,6 +1555,14 @@ CompUnit CompilationUnit() :
     cu = new CompUnit(pkg, firstToken != null ? new Location(firstToken) : new Location(currentFile,1,1), moduleName);
   }
   
+  (t=<IMPORTS> { if (firstToken == null) firstToken = t;
+                 if (moduleName == null) ErrorHandler.recoverableError(Errors.IMPORTS_IN_MODULE,new Location(t)); }
+    (
+      LOOKAHEAD( ("terminals" | "syntax" | "judgment" | "theorem" | "lemma") )
+      p=Part(false) {  cu.addImportChunk(p); }
+    )+
+  )?
+
   (t=<REQUIRES> { if (firstToken == null) firstToken = t;
                   if (moduleName == null) ErrorHandler.recoverableError(Errors.REQUIRES_IN_MODULE,new Location(t)); }
     (
diff --git a/src/edu/cmu/cs/sasylf/util/Errors.java b/src/edu/cmu/cs/sasylf/util/Errors.java
index 1eb12b90..09c7a36f 100644
--- a/src/edu/cmu/cs/sasylf/util/Errors.java
+++ b/src/edu/cmu/cs/sasylf/util/Errors.java
@@ -22,10 +22,12 @@ public enum Errors {
 	PARSE_EXPECTED_DERIVATION ("expected at least one derivation here"),
 	LEXICAL_ERROR ("Lexical error: "),
 	REQUIRES_IN_MODULE ("'requires' legal only for explicit modules"),
+	IMPORTS_IN_MODULE ("'imports' legal only for explicit modules"),
 	EXTENDS_IN_MODULE ("'extends' legal only for explicit modules"),
 	EXTENDS_UNIMPLEMENTED ("module 'extends' not implemented yet"),
 	PROVIDES_IN_MODULE ("'provides' legal only for explicit modules"),
 	PROVIDES_NOT_IN_MODULE ("'provides' expected for explicit modules"),
+	IMPORT_IN_REQUIRES ("module import (using '= QualName') should be in an 'imports' section, not 'requires'"),
 	ABSTRACT_NOT_PERMITTED_HERE ("'abstract' not allowed in main part of proof file"),
 	SYNTAX_DUPLICATE ("syntax nonterminal duplicate"),
 	JUDGMENT_ABSTRACT ("abstract judgment cannot have rules"),