diff --git a/bin/linja b/bin/linja
index d0ce42e191..35a1d938da 100755
--- a/bin/linja
+++ b/bin/linja
@@ -244,6 +244,10 @@ def get_lean_options(args):
     args.lean_options = []
     if args.flycheck:
         args.lean_options.append("--flycheck")
+    if args.discard:
+        args.lean_options.append("--discard")
+    if args.to_axiom:
+        args.lean_options.append("--to_axiom")
     if args.cache:
         args.lean_options += ["-c", args.cache]
     if args.lean_config_option:
@@ -260,6 +264,8 @@ def parse_arg(argv):
     parser.add_argument('--lean-config-option', '-D', action='append', help="set a Lean configuration option (name=value)")
     parser.add_argument('--verbose', '-v', action='store_true', help="turn on verbose option")
     parser.add_argument('--keep-going', '-k', action='store', default=None, const=1, nargs='?', help="keep going until N jobs fail [default=1]")
+    parser.add_argument('--discard', '-T', action='store_true', default=False, help="discard the proof of imported theorems after checking")
+    parser.add_argument('--to_axiom', '-X', action='store_true', default=False, help="discard proofs of all theorems after checking them, i.e., theorems become axioms after checking")
     parser.add_argument('targets', nargs='*')
     args = parser.parse_args(argv)
     check_requirements()