diff --git a/thys/FOL_Seq_Calc2/Dockerfile b/thys/FOL_Seq_Calc2/Dockerfile
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc2/Dockerfile
@@ -0,0 +1,75 @@
+# syntax=docker/dockerfile:1
+
+FROM makarius/isabelle AS builder
+
+USER root
+
+# install dependencies
+RUN \
+    apt-get update -y && \
+    apt-get install -y --no-install-recommends \
+        curl \
+        libnuma-dev \
+        zlib1g-dev \
+        libgmp-dev \
+        libgmp10 \
+        git \
+        wget \
+        lsb-release \
+        software-properties-common \
+        gnupg2 \
+        apt-transport-https \
+        gcc \
+        autoconf \
+        automake \
+        build-essential \
+	texlive-luatex \
+	texlive-latex-base \
+	texlive-plain-generic \
+	texlive-latex-recommended \
+	texlive-fonts-recommended
+
+# install ghcup
+RUN \
+    curl https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup > /usr/bin/ghcup && \
+    chmod +x /usr/bin/ghcup
+
+ARG GHC=9.4.2
+ARG CABAL=3.8.1.0
+
+# install GHC and cabal
+RUN \
+    ghcup -v install ghc --isolate /usr/local --force ${GHC} && \
+    ghcup -v install cabal --isolate /usr/local/bin --force ${CABAL}
+
+USER isabelle
+
+# set up Isabelle
+ENV PATH="$PATH:/home/isabelle/Isabelle/bin"
+
+# set up the AFP
+
+RUN curl https://www.isa-afp.org/release/afp-current.tar.gz > afp-current.tar.gz && \
+    tar xzf afp-current.tar.gz && \
+    rm afp-current.tar.gz && \
+    mv afp-* afp && \
+    isabelle components -u /home/isabelle/afp/thys
+
+WORKDIR /home/isabelle/secav-prover
+
+USER root
+RUN chown -R isabelle:isabelle /home/isabelle/secav-prover
+USER isabelle
+
+COPY --chown=isabelle  . .
+
+RUN cabal update
+RUN make
+RUN cabal install secav-prover
+
+FROM ubuntu:22.04
+
+WORKDIR /root/
+COPY --from=builder /home/isabelle/.cabal/bin/secav-prover ./
+
+ENTRYPOINT ["./secav-prover"]
diff --git a/thys/FOL_Seq_Calc2/README.md b/thys/FOL_Seq_Calc2/README.md
--- a/thys/FOL_Seq_Calc2/README.md
+++ b/thys/FOL_Seq_Calc2/README.md
@@ -1,232 +1,267 @@
 # SeCaV Prover
 This is an automated theorem prover for the SeCaV system for first-order logic with functions.
 
 It has been formally verified to be sound and complete, which means that it will never pretend to have proven an invalid formula, and that it will prove any valid formula if given enough time.
 The SeCaV Prover produces human-readable proofs in the SeCaV system, which means that users can verify the proofs by hand, and study them to understand why a formula is valid.
 
 The prover is implemented and verified in Isabelle, with some supporting functions implemented in Haskell.
 
 ## Installation
-You can download an executable binary version of the prover from the [release section](https://github.com/fkj/secav-prover/releases) of the development repository, or you can compile one yourself.
+You can download an executable version of the prover (either as a Linux binary or a Docker image) from the [release section](https://github.com/fkj/secav-prover/releases) of the development repository, or you can compile one yourself.
+Please see the [development repository](https://github.com/fkj/secav-prover) for the newest version.
+
+### Running via Docker
+If you do not want to (or cannot) install the prover directly on your machine, you can run the prover in a [Docker](https://www.docker.com/) container.
+To do this you will need to have Docker installed on your machine.
+
+You can either download a ready-to-use Docker image from the release section of the repository or build your own image (see below).
+If you have downloaded a Docker image from the release section, you can load it by running
+```
+docker load -i secav-prover-docker-image.tar.gz
+```
+
+Once you have a Docker image with the prover, you can run the prover inside a Docker container using e.g.
+```
+docker run secav-prover "Imp P P"
+```
+
+If you would like the prover to write Isabelle proof files (using the `--isabelle` option), you will need to give the Docker container access to a directory on your machine.
+You can give the container access to the current working directory and make the prover write an Isabelle proof file to it by running e.g.
+```
+docker run -v .:/outside secav-prover "Imp P P" --isabelle /outside/Proof.thy
+```
+
+#### Building a Docker image
+To build your own Docker image, simply run the following command inside the repository directory:
+```
+docker build -t secav-prover .
+```
+This will take a while, but you should eventually end up with a Docker image containing the prover.
+
+If you need to share your Docker image, you can export it using
+```
+docker save -o secav-prover-docker-image.tar secav-prover
+```
+This image can then be loaded using the instructions above (even if it is first compressed using e.g. gzip).
 
 ### Compilation
 The prover is implemented in Isabelle and Haskell.
 
 To compile the prover, you will need the following:
 * [The Isabelle proof assistant (isabelle)](https://isabelle.in.tum.de/)
 * [The Glasgow Haskell compiler (ghc)](https://www.haskell.org/ghc/)
 * [The Cabal build system (cabal)](https://www.haskell.org/cabal/)
 * [The Make build system (make)](https://www.gnu.org/software/make/)
 
 If you are on a Linux system, most of these can probably be installed through the package manager of your distribution.
 Otherwise, you will have to manually install each of them following the instructions on the pages linked above.
 If you are on Windows, you may additionally want a Cygwin installation to get a Unix-like environment.
 
 Additionally, the [Archive of Formal Proof](https://www.isa-afp.org/) must be installed and available to Isabelle.
 The ["Using Entries"](https://www.isa-afp.org/using.html) section of the linked page contains instructions on how to do this.
 
 If all of these are available, the prover can be compiled by invoking `make`.
 This will first build the Isabelle theory, which involves checking the proofs of soundness and completeness, then exporting the prover into Haskell code.
 The Cabal build system will then be called on to compile and link the exported code with the supporting (hand-written) Haskell code.
 This will produce an executable binary somewhere in the `dist-newstyle` folder.
 
 You can test that the prover works correctly by invoking `make test`.
 This will start two automated test suites consisting of integration tests for soundness and completeness.
 Since the Isabelle implementation of the prover has been formally verified to be sound and complete, these tests are mostly for the Haskell parts of the prover.
 Note that especially the completeness test suite may take quite a while to run since it involves processing many Isabelle theories.
 
 You can now run the prover through the `cabal run` command, e.g.
 ```
 cabal run secav-prover -- "Imp P P"
 ```
 In the usage examples below, simply replace `secav-prover` with `cabal run secav-prover --` to obtain equivalent results.
 
 If you want to, you can also install the prover using the command `cabal install secav-prover`.
 The command `secav-prover` should then become available on your PATH.
 
 ## Usage
 The prover can be run by providing it with a formula in SeCaV Unshortener syntax, e.g.:
 ```
 secav-prover "Imp P P"
 ```
 If the formula is valid, the prover will then output a proof of the formula in SeCaV Unshortener syntax on standard output.
 If the formula is not valid, the prover will loop forever, possibly printing parts of the failed proof tree as it goes.
 For proof-theoretical reasons, there is generally no way to determine whether the prover is working on a proof that may still finish or is in an infinite loop.
 For small formulas, however, the prover should finish very quickly if the formula is valid.
 
 If you would like the proof in Isabelle syntax instead, you may give a filename to write an Isabelle proof to using the `-i` (or `--isabelle`) switch, e.g.:
 ```
 secav-prover "Imp P P" -i Proof.thy
 ```
 The generated file can then be opened in Isabelle to verify the proof.
 To do so, the SeCaV theory must be available to Isabelle, e.g. by placing a copy of the `SeCaV.thy` file in the same folder as the generated file.
 
 ## Organisation of the repository
 The implementation of the prover is split into two main parts: the top folder contains the implementation of the proof search procedure itself as well as the formal proofs of soundness and completeness in Isabelle files (`.thy`), while the `haskell` folder contains implementations of supporting functions such as parsing and code generation.
 
 The top folder contains the following theories:
 * `SeCaV.thy` contains the definition of the Sequent Calculus Verifier system, which is the logic we are working in, and a soundness theorem for the proof system
 * `Sequent1.thy` is a shim theory for linking the AFP theory to the `Sequent_Calculus_Verifier` theory
 * `Sequent_Calculus_Verifier.thy` contains a completeness result for the SeCaV proof system
 * `Prover.thy` contains the definition of the proof search procedure
 * `Export.thy` contains the configuration of the Isabelle-to-Haskell code generator for the proof search procedure
 * `ProverLemmas.thy` contains formal proofs of a number of useful properties of the proof search procedure
 * `Hintikka.thy` contains a definition of Hintikka sets for SeCaV formulas
 * `EPathHintikka.thy` contains formal proof that the sets of formulas in infinite proof trees produced by the proof search procedure are Hintikka sets
 * `Usemantics.thy` contains a definition of an alternative bounded semantics for SeCaV, which is used in the completeness proof
 * `Countermodel.thy` contains a formal proof that an infinite proof tree produced by the proof search procedure gives rise to a countermodel of the formula given to the procedure
 * `Soundness.thy` contains a formal proof of the soundness of the proof search procedure
 * `Completeness.thy` contains a formal proof of the completeness of the proof search procedure
 * `Results.thy` contains a summary of our theorems as well as some extra results linking the proof system, the SeCaV semantics, and the bounded semantics
 
 The `haskell` folder initially contains two subfolders:
 * `lib` contains a parser for SeCaV Unshortener syntax, an Unshortener to SeCaV/Isabelle syntax, and a procedure for converting proof trees into SeCaV Unshortener proofs
 * `app` contains a definition of the command line interface of the prover
 
 The Isabelle code generation will create a third subfolder, `prover`, which contains the generated proof search procedure in Haskell.
 
 The `test` folder contains the definitions of the automated test suites for soundness and completeness.
 The files `secav-prover.cabal` and `Setup.hs` are used to configure the Cabal build system.
 The file `.hlint.yaml` is used to configure the HLint tool to ignore the generated Haskell code.
 
 ## Examples
 A very simple example is the one used above:
 ```
 > secav-prover "Imp P P"
 
 Imp P P
 
 AlphaImp
   Neg P
   P
 Ext
   P
   Neg P
 Basic
 ```
 
 If we add the `--isabelle Imp.thy` option, we instead obtain a file containing:
 ```
 theory Imp imports SeCaV begin
 
 proposition \<open>P \<longrightarrow> P\<close> by metis
 
 text \<open>
   Predicate numbers
 
     0 = P
   \<close>
 
 lemma \<open>\<tturnstile>
   [
     Imp (Pre 0 []) (Pre 0 [])
   ]
   \<close>
 proof -
   from AlphaImp have ?thesis if \<open>\<tturnstile>
     [
       Neg (Pre 0 []),
       Pre 0 []
     ]
     \<close>
     using that by simp
   with Ext have ?thesis if \<open>\<tturnstile>
     [
       Pre 0 [],
       Neg (Pre 0 [])
     ]
     \<close>
     using that by simp
   with Basic show ?thesis
     by simp
 qed
 
 end
 ```
 
 The prover works in first-order logic with functions, so we can also try:
 ```
 > secav-prover "Imp (Uni p[0]) (Exi (p[f[0]]))"
 Imp (Uni (p [0])) (Exi (p [f[0]]))
 
 AlphaImp
   Neg (Uni (p [0]))
   Exi (p [f[0]])
 Ext
   Exi (p [f[0]])
   Exi (p [f[0]])
   Neg (Uni (p [0]))
 GammaExi[f[0]]
   p [f[f[0]]]
   Exi (p [f[0]])
   Neg (Uni (p [0]))
 Ext
   Exi (p [f[0]])
   Exi (p [f[0]])
   Neg (Uni (p [0]))
   p [f[f[0]]]
 GammaExi[0]
   p [f[0]]
   Exi (p [f[0]])
   Neg (Uni (p [0]))
   p [f[f[0]]]
 Ext
   Neg (Uni (p [0]))
   Neg (Uni (p [0]))
   Exi (p [f[0]])
   p [f[f[0]]]
   p [f[0]]
 GammaUni[f[f[0]]]
   Neg (p [f[f[0]]])
   Neg (Uni (p [0]))
   Exi (p [f[0]])
   p [f[f[0]]]
   p [f[0]]
 Ext
   Neg (Uni (p [0]))
   Neg (Uni (p [0]))
   Exi (p [f[0]])
   p [f[f[0]]]
   p [f[0]]
   Neg (p [f[f[0]]])
 GammaUni[f[0]]
   Neg (p [f[0]])
   Neg (Uni (p [0]))
   Exi (p [f[0]])
   p [f[f[0]]]
   p [f[0]]
   Neg (p [f[f[0]]])
 Ext
   Neg (Uni (p [0]))
   Neg (Uni (p [0]))
   Exi (p [f[0]])
   p [f[f[0]]]
   p [f[0]]
   Neg (p [f[f[0]]])
   Neg (p [f[0]])
 GammaUni[0]
   Neg (p [0])
   Neg (Uni (p [0]))
   Exi (p [f[0]])
   p [f[f[0]]]
   p [f[0]]
   Neg (p [f[f[0]]])
   Neg (p [f[0]])
 Ext
   p [f[f[0]]]
   p [f[0]]
   Neg (Uni (p [0]))
   Neg (p [f[f[0]]])
   Neg (p [f[0]])
   Neg (p [0])
   Exi (p [f[0]])
 Basic
 ```
 
 ## Authors and license
 Developers:
 * [Asta Halkjær From](http://people.compute.dtu.dk/ahfrom/)
 * [Frederik Krogsdal Jacobsen](http://people.compute.dtu.dk/fkjac/)
 
 The prover is licensed under the GNU General Public License, version 3.0.
 See the `LICENSE` file for the text of the license.
diff --git a/thys/FOL_Seq_Calc2/ROOT b/thys/FOL_Seq_Calc2/ROOT
--- a/thys/FOL_Seq_Calc2/ROOT
+++ b/thys/FOL_Seq_Calc2/ROOT
@@ -1,25 +1,23 @@
-chapter AFP
-
-session FOL_Seq_Calc2 = "HOL-Library" +
-  options [timeout = 300]
+session SeCaV_Prover = "HOL-Library" +
+  options [document = pdf, document_output = "output", timeout = 300]
   sessions
     Collections
     Abstract_Completeness
     Abstract_Soundness
     FOL_Seq_Calc1
   theories
     SeCaV
     Sequent1
     Sequent_Calculus_Verifier
     Prover
     Export
     ProverLemmas
     Hintikka
     EPathHintikka
     Usemantics
     Countermodel
     Soundness
     Completeness
     Results
   document_files
     "root.tex"
diff --git a/thys/FOL_Seq_Calc2/document/root.tex b/thys/FOL_Seq_Calc2/document/root.tex
--- a/thys/FOL_Seq_Calc2/document/root.tex
+++ b/thys/FOL_Seq_Calc2/document/root.tex
@@ -1,68 +1,70 @@
 \documentclass[11pt,a4paper]{report}
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
+\usepackage[T1]{fontenc}
+
 \usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 %\usepackage{eurosym}
   %for \<euro>
 
 %\usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 %\usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 
 \begin{document}
 
 \title{A Sequent Calculus Prover for First-Order Logic with Functions}
 \author{Asta Halkjær From \and Frederik Krogsdal Jacobsen}
 \maketitle
 
 \begin{abstract}
 	We formalize an automated theorem prover for first-order logic with functions.
 	The proof search procedure is based on sequent calculus and we verify its soundness and completeness using the Abstract Soundness and Abstract Completeness theories.
 	Our analytic completeness proof covers both open and closed formulas.
 	Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do so as well when building a countermodel from a failed proof.
 	We formally connect our prover with the proof system and semantics of the existing SeCaV system.
 	In particular, the prover's output can be post-processed in Haskell to generate human-readable SeCaV proofs which are also machine-verifiable proof certificates.
 \end{abstract}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/FOL_Seq_Calc2/haskell/lib/ProofExtractor.hs b/thys/FOL_Seq_Calc2/haskell/lib/ProofExtractor.hs
--- a/thys/FOL_Seq_Calc2/haskell/lib/ProofExtractor.hs
+++ b/thys/FOL_Seq_Calc2/haskell/lib/ProofExtractor.hs
@@ -1,423 +1,427 @@
 {-# LANGUAGE FlexibleInstances #-}
 
 module ProofExtractor where
 
 import Arith ( Nat(Nat), zero_nat )
 import qualified Data.Bimap as Map
 import Control.Monad.State (evalState, get, modify)
 import Data.List (genericReplicate, intercalate)
 import FSet ( Fset(Abs_fset) )
 import Prover ( Rule(..), Tree(..), generateNew)
 import ProverInstances()
 import SeCaV ( Fm(..), Tm(..), sub )
 import Set ( Set(Set, Coset) )
 import ShortAST (funCount, NameGen,  NameState(existingFuns, existingPres) )
 
 -- These are the "real" rules of SeCaV that we want to end up with
 data SeCaVRule
   = RBasic
   | RAlphaDis
   | RAlphaImp
   | RAlphaCon
   | RBetaCon
   | RBetaImp
   | RBetaDis
   | RGammaExi Tm
   | RGammaUni Tm
   | RDeltaUni
   | RDeltaExi
   | RNeg
   | RExt
   deriving (Show)
 
 instance Show (Set (Tree ([Fm], SeCaVRule))) where
   show (Set s) = show s
   show (Coset s) = show s
 
 instance Show (Fset (Tree ([Fm], SeCaVRule))) where
   show (Abs_fset s) = show s
 
 instance Show (Tree ([Fm], SeCaVRule)) where
   show (Node (fs, r) t) = show fs <> " " <> show r <> "\n" <> show t
 
 -- These functions get every first and every second element of a list, respectively
 -- They are used to split the cartesian product of branches from Beta rules into binary trees
 first :: [a] -> [a]
 first [] = []
 first (x : xs) = x : second xs
 
 second :: [a] -> [a]
 second [] = []
 second (_ : xs) = first xs
 
 -- Expansion of the alpha, delta, and double negation elimination rules
 expandAlphaDelta :: Tree (([Tm], [Fm]), Rule) -> Int -> Tree ([Fm], SeCaVRule)
 expandAlphaDelta (Node ((terms, f : fs), rule) (Abs_fset (Set [current]))) n =
-  let (srule, applied) = case (rule, f) of
-                  (AlphaDis, Dis p q) -> (RAlphaDis, [p, q])
-                  (AlphaCon, Neg (Con p q)) -> (RAlphaCon, [Neg p, Neg q])
-                  (AlphaImp, Imp p q) -> (RAlphaImp, [Neg p, q])
-                  (NegNeg, Neg (Neg p)) -> (RNeg, [p])
-                  (DeltaUni, Uni p) -> (RDeltaUni, [SeCaV.sub Arith.zero_nat (SeCaV.Fun (generateNew terms) []) p])
-                  (DeltaExi, Neg (Exi p)) -> (RDeltaExi, [Neg (SeCaV.sub Arith.zero_nat (SeCaV.Fun (generateNew terms) []) p)])
-                  (AlphaDis, x) -> (RAlphaDis, [x])
-                  (AlphaCon, x) -> (RAlphaCon, [x])
-                  (AlphaImp, x) -> (RAlphaImp, [x])
-                  (DeltaUni, x) -> (RDeltaUni, [x])
-                  (DeltaExi, x) -> (RDeltaExi, [x])
-                  (NegNeg, x) -> (RNeg, [x])
+  let (srule, applied, newTerms) = case (rule, f) of
+                  (AlphaDis, Dis p q) -> (RAlphaDis, [p, q], [])
+                  (AlphaCon, Neg (Con p q)) -> (RAlphaCon, [Neg p, Neg q], [])
+                  (AlphaImp, Imp p q) -> (RAlphaImp, [Neg p, q], [])
+                  (NegNeg, Neg (Neg p)) -> (RNeg, [p], [])
+                  (DeltaUni, Uni p) ->
+                    let newFun = SeCaV.Fun (generateNew terms) [] in
+                      (RDeltaUni, [SeCaV.sub Arith.zero_nat newFun p], [newFun])
+                  (DeltaExi, Neg (Exi p)) ->
+                    let newFun = SeCaV.Fun (generateNew terms) [] in
+                      (RDeltaExi, [Neg (SeCaV.sub Arith.zero_nat newFun p)], [newFun])
+                  (AlphaDis, x) -> (RAlphaDis, [x], [])
+                  (AlphaCon, x) -> (RAlphaCon, [x], [])
+                  (AlphaImp, x) -> (RAlphaImp, [x], [])
+                  (DeltaUni, x) -> (RDeltaUni, [x], [])
+                  (DeltaExi, x) -> (RDeltaExi, [x], [])
+                  (NegNeg, x) -> (RNeg, [x], [])
                   _ -> error "expandAlphaDelta must only be called on Alpha, Neg or Delta rules." in
   let extRule = if n == 1
         then Node (applied ++ fs, RExt) (Abs_fset (Set [expandMultiRules current]))
-        else Node (applied ++ fs, RExt) (Abs_fset (Set [expandAlphaDelta (Node ((terms, fs ++ applied), rule) (Abs_fset (Set [current]))) (n - 1)])) in
+        else Node (applied ++ fs, RExt) (Abs_fset (Set [expandAlphaDelta (Node ((terms ++ newTerms, fs ++ applied), rule) (Abs_fset (Set [current]))) (n - 1)])) in
   Node (f : fs, srule) (Abs_fset (Set [extRule]))
 expandAlphaDelta (Node ((_, []), _) _) _ = error "The sequent must never be empty."
 expandAlphaDelta (Node ((_, _), _) (Abs_fset (Coset _))) _ = error "The proof tree must not include cosets."
 expandAlphaDelta (Node ((_, _), _) (Abs_fset (Set _))) _ = error "Alpha, Neg, and Delta rules must produce exactly one branch."
 
 betaNonRuleN :: Rule -> Fm -> [Fm] -> [Tm] -> [Tree (([Tm], [Fm]), Rule)] -> Int -> Tree ([Fm], SeCaVRule)
 betaNonRuleN rule f fs terms rest n = Node (f : fs, RExt) (Abs_fset (Set [expandBeta (Node ((terms, fs ++ [f]), rule) (Abs_fset (Set rest))) (n - 1)]))
 
 betaRuleN :: Rule -> Fm -> [Fm] -> [Tm] -> [Tree (([Tm], [Fm]), Rule)] -> Int -> Tree ([Fm], SeCaVRule)
 betaRuleN rule f fs terms branches n = Node (f : fs, RExt) (Abs_fset (Set [expandBeta (Node ((terms, fs ++ [f]), rule) (Abs_fset (Set branches))) (n - 1)]))
 
 betaRule1 :: Fm -> [Fm] -> Tree (([Tm], [Fm]), Rule) -> Tree ([Fm], SeCaVRule)
 betaRule1 f fs branch = Node (f : fs, RExt) (Abs_fset (Set [expandMultiRules branch]))
 
 -- Expansion of BetaCon rule
 -- The prover creates the product of all beta rules as branches, so we need to reassemble the branches into a binary tree
 expandBeta :: Tree (([Tm], [Fm]), Rule) -> Int -> Tree ([Fm], SeCaVRule)
 expandBeta (Node ((_, Con p q : fs), BetaCon) (Abs_fset (Set [b1, b2]))) 1 =
   let branch1 = betaRule1 p fs b1 in
   let branch2 = betaRule1 q fs b2 in
   Node (Con p q : fs, RBetaCon) (Abs_fset (Set [branch1, branch2]))
 expandBeta (Node ((_, Neg (Imp p q) : fs), BetaImp) (Abs_fset (Set [b1, b2]))) 1 =
   let branch1 = betaRule1 p fs b1 in
   let branch2 = betaRule1 (Neg q) fs b2 in
   Node (Neg (Imp p q) : fs, RBetaImp) (Abs_fset (Set [branch1, branch2]))
 expandBeta (Node ((_, Neg (Dis p q) : fs), BetaDis) (Abs_fset (Set [b1, b2]))) 1 =
   let branch1 = betaRule1 (Neg p) fs b1 in
   let branch2 = betaRule1 (Neg q) fs b2 in
   Node (Neg (Dis p q) : fs, RBetaDis) (Abs_fset (Set [branch1, branch2]))
 expandBeta (Node ((_, f : fs), BetaCon) (Abs_fset (Set [current]))) 1 =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   Node (f : fs, RBetaCon) (Abs_fset (Set [extRule]))
 expandBeta (Node ((_, f : fs), BetaImp) (Abs_fset (Set [current]))) 1 =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   Node (f : fs, RBetaImp) (Abs_fset (Set [extRule]))
 expandBeta (Node ((_, f : fs), BetaDis) (Abs_fset (Set [current]))) 1 =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   Node (f : fs, RBetaDis) (Abs_fset (Set [extRule]))
 expandBeta (Node ((terms, Con p q : fs), BetaCon) (Abs_fset (Set branches))) n =
   let branch1 = betaRuleN BetaCon p fs terms (first branches) n in
   let branch2 = betaRuleN BetaImp q fs terms (second branches) n in
   Node (Con p q : fs, RBetaCon) (Abs_fset (Set [branch1, branch2]))
 expandBeta (Node ((terms, Neg (Imp p q) : fs), BetaImp) (Abs_fset (Set branches))) n =
   let branch1 = betaRuleN BetaImp p fs terms (first branches) n in
   let branch2 = betaRuleN BetaImp (Neg q) fs terms (second branches) n in
   Node (Neg (Imp p q) : fs, RBetaImp) (Abs_fset (Set [branch1, branch2]))
 expandBeta (Node ((terms, Neg (Dis p q) : fs), BetaDis) (Abs_fset (Set branches))) n =
   let branch1 = betaRuleN BetaDis (Neg p) fs terms (first branches) n in
   let branch2 = betaRuleN BetaDis (Neg q) fs terms (second branches) n in
   Node (Neg (Dis p q) : fs, RBetaDis) (Abs_fset (Set [branch1, branch2]))
 expandBeta (Node ((terms, f : fs), BetaCon) (Abs_fset (Set rest))) n =
   let extRule = betaNonRuleN BetaCon f fs terms rest n in
   Node (f : fs, RBetaCon) (Abs_fset (Set [extRule]))
 expandBeta (Node ((terms, f : fs), BetaImp) (Abs_fset (Set rest))) n =
   let extRule = betaNonRuleN BetaImp f fs terms rest n in
   Node (f : fs, RBetaImp) (Abs_fset (Set [extRule]))
 expandBeta (Node ((terms, f : fs), BetaDis) (Abs_fset (Set rest))) n =
   let extRule = betaNonRuleN BetaDis f fs terms rest n in
   Node (f : fs, RBetaDis) (Abs_fset (Set [extRule]))
 expandBeta (Node ((_, []), _) _) _ = error "The sequent must never be empty."
 expandBeta (Node ((_, _), _) (Abs_fset (Coset _))) _ = error "The proof tree must not include cosets."
 expandBeta (Node ((_, _), _) (Abs_fset (Set []))) _ = error "Beta rules must always produce at least one branch."
 expandBeta (Node ((_, _), _) (Abs_fset (Set [_]))) _ = error "expandBeta must only be called on Beta rules."
 expandBeta (Node ((_, _), _) (Abs_fset (Set [_, _]))) _ = error "expandBeta must only be called on Beta rules."
 expandBeta (Node ((_, _), _) (Abs_fset (Set (_ : _ : _ : _)))) _ = error "Beta must never produce more than two branches."
 
 -- Expansion of GammaExi rule
 -- Here we have a counter for the sequent formulas (ns) and a counter for the terms (nt) since we need to instantiate each formula with each term
 expandGammaExi :: Tree (([Tm], [Fm]), Rule) -> Int -> Int -> Tree ([Fm], SeCaVRule)
 expandGammaExi (Node ((t : _, Exi p : fs), GammaExi) (Abs_fset (Set [current]))) 1 1 =
   let applied = SeCaV.sub Arith.zero_nat t p in
   let extRule = Node (applied : Exi p : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   let gammaRule = Node (Exi p : Exi p : fs, RGammaExi t) (Abs_fset (Set [extRule])) in
   Node (Exi p : fs, RExt) (Abs_fset (Set [gammaRule]))
 expandGammaExi (Node ((t : ts, Exi p : fs), GammaExi) (Abs_fset (Set [current]))) ns 1 =
   let applied = SeCaV.sub Arith.zero_nat t p in
   let extRule = Node (applied : Exi p : fs, RExt) (Abs_fset (Set [expandGammaExi (Node ((ts ++ [t], fs ++ [applied, Exi p]), GammaExi) (Abs_fset (Set [current]))) (ns - 1) (length (t : ts))])) in
   let gammaRule = Node (Exi p : Exi p : fs, RGammaExi t) (Abs_fset (Set [extRule])) in
   Node (Exi p : fs, RExt) (Abs_fset (Set [gammaRule]))
 expandGammaExi (Node ((t : ts, Exi p : fs), GammaExi) (Abs_fset (Set [current]))) ns nt =
   let applied = SeCaV.sub Arith.zero_nat t p in
   let extRule = Node (applied : Exi p : fs, RExt) (Abs_fset (Set [expandGammaExi (Node ((ts ++ [t], Exi p : fs ++ [applied]), GammaExi) (Abs_fset (Set [current]))) ns (nt - 1)])) in
   let gammaRule = Node (Exi p : Exi p : fs, RGammaExi t) (Abs_fset (Set [extRule])) in
   Node (Exi p : fs, RExt) (Abs_fset (Set [gammaRule]))
 expandGammaExi (Node ((t : _, f : fs), GammaExi) (Abs_fset (Set [current]))) 1 _ =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   Node (f : fs, RGammaExi t) (Abs_fset (Set [extRule]))
 expandGammaExi (Node ((t : ts, f : fs), GammaExi) (Abs_fset (Set [current]))) ns nt =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandGammaExi (Node ((t : ts, fs ++ [f]), GammaExi) (Abs_fset (Set [current]))) (ns - 1) nt])) in
   Node (f : fs, RGammaExi t) (Abs_fset (Set [extRule]))
 expandGammaExi (Node ((_, []), _) _) _ _ = error "The sequent must never be empty."
 expandGammaExi (Node ((_, _), _) (Abs_fset (Coset _))) _ _ = error "The proof tree must not include cosets."
 expandGammaExi (Node ((_, _), _) (Abs_fset (Set [_]))) _ _ = error "expandGammaExi must only be called on GammaExi rules."
 expandGammaExi (Node ((_, _), _) (Abs_fset (Set []))) _ _ = error "GammaExi rules must produce exactly one branch."
 expandGammaExi (Node ((_, _), _) (Abs_fset (Set (_ : _ : _)))) _ _ = error "GammaExi rules must produce exactly one branch."
 
 -- Expansion of GammaUni rule
 -- Here we have a counter for the sequent formulas (ns) and a counter for the terms (nt) since we need to instantiate each formula with each term
 expandGammaUni :: Tree (([Tm], [Fm]), Rule) -> Int -> Int -> Tree ([Fm], SeCaVRule)
 expandGammaUni (Node ((t : _, Neg (Uni p) : fs), GammaUni) (Abs_fset (Set [current]))) 1 1 =
   let applied = Neg (SeCaV.sub Arith.zero_nat t p) in
   let extRule = Node (applied : Neg (Uni p) : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   let gammaRule = Node (Neg (Uni p) : Neg (Uni p) : fs, RGammaUni t) (Abs_fset (Set [extRule])) in
   Node (Neg (Uni p) : fs, RExt) (Abs_fset (Set [gammaRule]))
 expandGammaUni (Node ((t : ts, Neg (Uni p) : fs), GammaUni) (Abs_fset (Set [current]))) ns 1 =
   let applied = Neg (SeCaV.sub Arith.zero_nat t p) in
   let extRule = Node (applied : Neg (Uni p) : fs, RExt) (Abs_fset (Set [expandGammaUni (Node ((ts ++ [t], fs ++ [applied, Neg (Uni p)]), GammaUni) (Abs_fset (Set [current]))) (ns - 1) (length (t : ts))])) in
   let gammaRule = Node (Neg (Uni p) : Neg (Uni p) : fs, RGammaUni t) (Abs_fset (Set [extRule])) in
   Node (Neg (Uni p) : fs, RExt) (Abs_fset (Set [gammaRule]))
 expandGammaUni (Node ((t : ts, Neg (Uni p) : fs), GammaUni) (Abs_fset (Set [current]))) ns nt =
   let applied = Neg (SeCaV.sub Arith.zero_nat t p) in
   let extRule = Node (applied : Neg (Uni p) : fs, RExt) (Abs_fset (Set [expandGammaUni (Node ((ts ++ [t], Neg (Uni p) : fs ++ [applied]), GammaUni) (Abs_fset (Set [current]))) ns (nt - 1)])) in
   let gammaRule = Node (Neg (Uni p) : Neg (Uni p) : fs, RGammaUni t) (Abs_fset (Set [extRule])) in
   Node (Neg (Uni p) : fs, RExt) (Abs_fset (Set [gammaRule]))
 expandGammaUni (Node ((t : _, f : fs), GammaUni) (Abs_fset (Set [current]))) 1 _ =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandMultiRules current])) in
   Node (f : fs, RGammaUni t) (Abs_fset (Set [extRule]))
 expandGammaUni (Node ((t : ts, f : fs), GammaUni) (Abs_fset (Set [current]))) ns nt =
   let extRule = Node (f : fs, RExt) (Abs_fset (Set [expandGammaUni (Node ((t : ts, fs ++ [f]), GammaUni) (Abs_fset (Set [current]))) (ns - 1) nt])) in
   Node (f : fs, RGammaUni t) (Abs_fset (Set [extRule]))
 expandGammaUni (Node ((_, []), _) _) _ _ = error "The sequent must never be empty."
 expandGammaUni (Node ((_, _), _) (Abs_fset (Coset _))) _ _ = error "The proof tree must not include cosets."
 expandGammaUni (Node ((_, _), _) (Abs_fset (Set [_]))) _ _ = error "expandGammaUni must only be called on GammaUni rules."
 expandGammaUni (Node ((_, _), _) (Abs_fset (Set []))) _ _ = error "GammaUni rules must produce exactly one branch."
 expandGammaUni (Node ((_, _), _) (Abs_fset (Set (_ : _ : _)))) _ _ = error "GammaUni rules must produce exactly one branch."
 
 -- This function moves the positive part of a Basic pair in the front of the sequent to allow the Basic rule to be applied
 -- WARNING: This will loop forever if there is no Basic pair (P and Neg P) in the sequent
 sortSequent :: [Fm] -> [Fm]
 sortSequent [] = []
 sortSequent (x : xs) = if Neg x `elem` xs then x : xs else sortSequent (xs ++ [x])
 
 -- This adds an Ext rule to move the Basic pair in position, then a Basic rule to end a branch
 addBasicRule :: Tree (([Tm], [Fm]), Rule) -> Tree ([Fm], SeCaVRule)
 addBasicRule (Node ((_, sequent), _) (Abs_fset (Set []))) =
   let basicRule = Node (sortSequent sequent, RBasic) (Abs_fset (Set [])) in
     Node (sequent, RExt) (Abs_fset (Set [basicRule]))
 addBasicRule (Node ((_, _), _) (Abs_fset (Coset _))) = error "The proof tree must not include cosets."
 addBasicRule (Node ((_, _), _) (Abs_fset (Set _))) = error "Basic rules must only be used to close branches."
 
 -- This function takes the rules from the prover and expands them into separate SeCaV applications for each formula in the sequent with Ext's in between
 -- Gamma rules are expanded for each formula and for each term
 -- Note that after this function, rules are still applied to all formulas, even those that do not fit the rule
 expandMultiRules :: Tree (([Tm], [Fm]), Rule) -> Tree ([Fm], SeCaVRule)
 expandMultiRules node@(Node _ (Abs_fset (Set []))) = addBasicRule node
 expandMultiRules node@(Node ((_, sequent), AlphaDis) _) = expandAlphaDelta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), AlphaCon) _) = expandAlphaDelta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), AlphaImp) _) = expandAlphaDelta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), NegNeg) _) = expandAlphaDelta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), BetaCon) _) = expandBeta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), BetaImp) _) = expandBeta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), BetaDis) _) = expandBeta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), DeltaUni) _) = expandAlphaDelta node (length sequent)
 expandMultiRules node@(Node ((_, sequent), DeltaExi) _) = expandAlphaDelta node (length sequent)
 expandMultiRules node@(Node ((terms, sequent), GammaExi) _) = expandGammaExi node (length sequent) (length terms)
 expandMultiRules node@(Node ((terms, sequent), GammaUni) _) = expandGammaUni node (length sequent) (length terms)
 
 -- This function removes all rule applications that do nothing (which includes all wrong rule applications)
 -- It should be called both before and after the extSurgery function to be sure to remove all extraneous Ext rules
 removeNoopRules :: Tree ([Fm], SeCaVRule) -> Tree ([Fm], SeCaVRule)
 removeNoopRules node@(Node (_, _) (Abs_fset (Set []))) = node
 removeNoopRules (Node (s1, r1) (Abs_fset (Set [Node (s2, r2) (Abs_fset (Set rest))]))) =
                                 if s1 == s2
                                 then removeNoopRules (Node (s2, r2) (Abs_fset (Set rest)))
                                 else Node (s1, r1) (Abs_fset (Set [removeNoopRules (Node (s2, r2) (Abs_fset (Set rest)))]))
 removeNoopRules (Node (s, r) (Abs_fset (Set rest))) = Node (s, r) (Abs_fset (Set (map removeNoopRules rest)))
 removeNoopRules (Node (_, _) (Abs_fset (Coset _))) = error "The proof tree must not include cosets."
 
 -- This function collapses successive applications of the Ext rule to a single application
 -- A lot of these will appear after eliminating rules that are applied to wrong formulas, so this shortens the proof quite a bit
 extSurgery :: Tree ([Fm], SeCaVRule) -> Tree ([Fm], SeCaVRule)
 extSurgery node@(Node (_, RExt) (Abs_fset (Set []))) = node
 extSurgery (Node (sequent, RExt) (Abs_fset (Set [Node (_, RExt) next@(Abs_fset (Set []))]))) =
   Node (sequent, RExt) next
 extSurgery (Node (sequent, RExt) (Abs_fset (Set [Node (_, RExt) (Abs_fset (Set [current]))]))) =
   extSurgery $ Node (sequent, RExt) (Abs_fset (Set [current]))
 extSurgery (Node (sequent, RExt) (Abs_fset (Set [Node (_, RExt) (Abs_fset (Set [current, next]))]))) =
   extSurgery $ Node (sequent, RExt) (Abs_fset (Set [current, next]))
 extSurgery node@(Node (_, _) (Abs_fset (Set []))) = node
 extSurgery (Node (s, r) (Abs_fset (Set [current]))) = Node (s, r) (Abs_fset (Set [extSurgery current]))
 extSurgery (Node (s, r) (Abs_fset (Set [current, next]))) = Node (s, r) (Abs_fset (Set [extSurgery current, extSurgery next]))
 extSurgery (Node _ (Abs_fset (Set (_ : _ : _ : _)))) = error "No proof rule should generate more than two branches."
 extSurgery (Node _ (Abs_fset (Coset _))) = error "No proof rule should generate a coset of branches."
 
 initExtract :: NameState -> Tree ([Fm], SeCaVRule) -> String
 initExtract names tree = evalState (extract tree) names
 
 extract :: Tree ([Fm], SeCaVRule) -> NameGen String
 extract (Node (sequent, rule) (Abs_fset (Set []))) = do
   s <- extractSequent sequent
   r <- extractRule rule
   pure $ s <> "\n\n" <> r <> "\n"
 extract (Node (sequent, rule) (Abs_fset (Set [current]))) = do
   s <- extractSequent sequent
   r <- extractRule rule
   c <- extract' [] current
   pure $ s <> "\n\n" <> r <> "\n" <> c
 extract (Node (sequent, rule) (Abs_fset (Set [current, next]))) = do
   s <- extractSequent sequent
   r <- extractRule rule
   c <- extract' [extractNextSequent next] current
   n <- extract' [] next
   pure $ s <> "\n\n" <> r <> "\n" <> c <> n
 extract _ =
   error "By the pricking of my thumbs, something wicked this way comes..."
 
 extract' :: [[Fm]] -> Tree ([Fm], SeCaVRule) -> NameGen String
 extract' other (Node (sequent, rule) (Abs_fset (Set []))) = do
   s <- extractSequent' sequent
   ss <- extractOtherSequents other
   r <- extractRule rule
   pure $ s <> (if null other then "" else "\n+\n" <> ss) <> "\n" <> r <> "\n"
 extract' other (Node (sequent, rule) (Abs_fset (Set [current]))) = do
   s <- extractSequent' sequent
   ss <- extractOtherSequents other
   r <- extractRule rule
   c <- extract' other current
   pure $ s <> (if null other then "" else "\n+\n" <> ss) <> "\n" <> r <> "\n" <> c
 extract' other (Node (sequent, rule) (Abs_fset (Set [current, next]))) = do
   s <- extractSequent' sequent
   ss <- extractOtherSequents other
   r <- extractRule rule
   n <- extract' (extractNextSequent next : other) current
   c <- extract' other next
   pure $ s <> (if null other then "" else "\n+\n" <> ss) <> "\n" <> r <> "\n" <> n <> c
 extract' _ _ =
   error "By the pricking of my thumbs, something wicked this way comes..."
 
 extractNextSequent :: Tree ([Fm], SeCaVRule) -> [Fm]
 extractNextSequent (Node (sequent, _) _) = sequent
 
 extractOtherSequents :: [[Fm]] -> NameGen String
 extractOtherSequents [] = pure ""
 extractOtherSequents [x] = extractSequent' x
 extractOtherSequents (x:xs) = do
   s <- extractSequent' x
   ss <- extractOtherSequents xs
   pure $ s <> "\n+\n" <> ss
 
 extractSequent :: [Fm] -> NameGen String
 extractSequent [] = pure ""
 extractSequent [x] = extractFormula x
 extractSequent (x:xs) = do
   f <- extractFormula x
   s <- extractSequent xs
   pure $ f <> "\n" <> s
 
 extractSequent' :: [Fm] -> NameGen String
 extractSequent' [] = pure ""
 extractSequent' [x] = do
   f <- extractFormula x
   pure $ "  " <> f
 extractSequent' (x:xs) = do
   f <- extractFormula x
   s <- extractSequent' xs
   pure $ "  " <> f <> "\n" <> s
 
 genName :: Integer -> String
 genName x | x < 0 = "?"
 genName 0 = "a"
 genName 1 = "b"
 genName 2 = "c"
 genName 3 = "d"
 genName 4 = "e"
 genName 5 = "f"
 genName x = "g" <> genericReplicate (x - 5) '\''
 
 genFunName :: Integer -> NameGen String
 genFunName n = do
   s <- get
   case Map.lookupR n (existingFuns s) of
     Just name -> pure name
     Nothing -> do
       let nameNum = until (\x -> Map.notMemberR x (existingFuns s)) (+ 1) 0
       let name = genName nameNum
       _ <- modify (\st -> st { funCount = funCount s + 1
                              , existingFuns = Map.insert name n (existingFuns s)
                              })
       pure $ genName nameNum
 
 extractTerm :: Tm -> NameGen String
 extractTerm (SeCaV.Fun (Nat n) []) = genFunName n
 extractTerm (SeCaV.Fun (Nat n) ts) = do
   fName <- genFunName n
   termNames <- traverse extractTerm ts
   pure $ fName <> "[" <> intercalate ", " termNames <> "]"
 extractTerm (SeCaV.Var n) = pure $ show n
 
 dropEnd :: Int -> String -> String
 dropEnd n = reverse . drop n . reverse
 
 extractFormula :: Fm -> NameGen String
 extractFormula (SeCaV.Pre (Nat n) []) = do
   s <- get
   pure $ existingPres s Map.!> n
 extractFormula (SeCaV.Pre (Nat n) ts) = do
   s <- get
   termNames <- traverse extractTerm ts
   pure $ existingPres s Map.!> n <> " [" <> intercalate ", " termNames <> "]"
 extractFormula f = do
   form <- extractFormula' f
   pure $ drop 1 $ dropEnd 1 form
 
 extractFormula' :: Fm -> NameGen String
 extractFormula' (SeCaV.Pre (Nat n) []) = do
   s <- get
   pure $ existingPres s Map.!> n
 extractFormula' (SeCaV.Pre (Nat n) ts) = do
   s <- get
   termNames <- traverse extractTerm ts
   pure $ "(" <> existingPres s Map.!> n <> " [" <> intercalate ", " termNames  <> "])"
 extractFormula' (SeCaV.Imp a b) = do
   formA <- extractFormula' a
   formB <- extractFormula' b
   pure $ "(Imp " <> formA <> " " <> formB <> ")"
 extractFormula' (SeCaV.Dis a b) = do
   formA <- extractFormula' a
   formB <- extractFormula' b
   pure $ "(Dis " <> formA <> " " <> formB <> ")"
 extractFormula' (SeCaV.Con a b) = do
   formA <- extractFormula' a
   formB <- extractFormula' b
   pure $ "(Con " <> formA <> " " <> formB <> ")"
 extractFormula' (SeCaV.Exi f) = do
   form <- extractFormula' f
   pure $ "(Exi " <> form <> ")"
 extractFormula' (SeCaV.Uni f) = do
   form <- extractFormula' f
   pure $ "(Uni " <> form <> ")"
 extractFormula' (SeCaV.Neg f) = do
   form <- extractFormula' f
   pure $ "(Neg " <> form <> ")"
 
 extractRule :: SeCaVRule -> NameGen String
 extractRule RBasic = pure "Basic"
 extractRule RAlphaDis = pure "AlphaDis"
 extractRule RAlphaImp = pure "AlphaImp"
 extractRule RAlphaCon = pure "AlphaCon"
 extractRule RBetaCon = pure"BetaCon"
 extractRule RBetaImp = pure "BetaImp"
 extractRule RBetaDis = pure "BetaDis"
 extractRule (RGammaUni t) = do
   termName <- extractTerm t
   pure $ "GammaUni[" <> termName <> "]"
 extractRule (RGammaExi t) = do
   termName <- extractTerm t
   pure $ "GammaExi[" <> termName <> "]"
 extractRule RDeltaUni = pure "DeltaUni"
 extractRule RDeltaExi = pure "DeltaExi"
 extractRule RNeg = pure "NegNeg"
 extractRule RExt = pure "Ext"
diff --git a/thys/FOL_Seq_Calc2/secav-prover.cabal b/thys/FOL_Seq_Calc2/secav-prover.cabal
--- a/thys/FOL_Seq_Calc2/secav-prover.cabal
+++ b/thys/FOL_Seq_Calc2/secav-prover.cabal
@@ -1,86 +1,86 @@
 cabal-version:       2.4
 name:                secav-prover
-version:             1.0.0.0
+version:             1.0.1.0
 synopsis:            Prover for the SeCaV system
 license:             GPL-3.0-only
 license-file:        LICENSE
 author:              Frederik Krogsdal Jacobsen
 maintainer:          fkjacobsen@gmail.com
 category:            Math
 description:         An automated theorem prover for the SeCaV system of first-order logic.
 build-type:          Simple
 
 source-repository head
   type:               git
   location:           git://github.com/fkj/secav-prover.git
 
 library prover
   exposed-modules:    Arith
                     , FSet
                     , Prover
                     , SeCaV
                     , Set
   other-modules:      Lazy
                     , List
                     , MaybeExt
                     , Orderings
                     , Product_Type
                     , HOL
   build-depends:      base
   hs-source-dirs:     haskell/prover
   default-language:   Haskell2010
 
 library interface
   exposed-modules:     ProofExtractor
                      , ProverInstances
                      , ShortAST
                      , SeCaVTranslator
                      , ShortLexer
                      , ShortParser
                      , Unshortener
-  build-depends:       base ^>=4.14.0.0
+  build-depends:       base ^>=4.17.0.0
                      , prover
                      , parsec
                      , bimap
                      , mtl
   hs-source-dirs:      haskell/lib
   default-language:    Haskell2010
   ghc-options:         -Wall
 
 test-suite completeness
   type:                detailed-0.9
   test-module:         Runner
   other-modules:       Tests
-  build-depends:       base ^>=4.14.0.0
+  build-depends:       base ^>=4.17.0.0
                      , Cabal >= 1.9.2
                      , process
                      , directory
                      , mtl
                      , prover
                      , interface
   hs-source-dirs:      test/completeness
   default-language:    Haskell2010
 
 test-suite soundness
   type:                detailed-0.9
   test-module:         Runner
   other-modules:       Tests
-  build-depends:       base ^>=4.14.0.0
+  build-depends:       base ^>=4.17.0.0
                      , Cabal >= 1.9.2
                      , process
                      , mtl
                      , prover
                      , interface
   hs-source-dirs:      test/soundness
   default-language:    Haskell2010
 
 executable secav-prover
   main-is:             Main.hs
-  build-depends:       base ^>=4.14.0.0
+  build-depends:       base ^>=4.17.0.0
                      , prover
                      , interface
                      , filepath
                      , optparse-applicative
   hs-source-dirs:      haskell/app
   default-language:    Haskell2010
   ghc-options:         -Wall
diff --git a/thys/FOL_Seq_Calc2/test/completeness/Runner.hs b/thys/FOL_Seq_Calc2/test/completeness/Runner.hs
--- a/thys/FOL_Seq_Calc2/test/completeness/Runner.hs
+++ b/thys/FOL_Seq_Calc2/test/completeness/Runner.hs
@@ -1,71 +1,71 @@
 module Runner (tests) where
 
 import Distribution.TestSuite
   ( Progress (Finished),
     Result (Fail, Pass),
     Test (Test),
     TestInstance (TestInstance, name, options, run, setOption, tags),
   )
 import ProofExtractor (initExtract, extSurgery, removeNoopRules, expandMultiRules)
 import Prover (secavProverCode)
 import SeCaVTranslator (genInit)
 import ShortParser (programParser, sequentParser)
 import System.Directory
   ( copyFile,
     createDirectoryIfMissing,
     removeDirectoryRecursive,
   )
 import System.Exit (ExitCode (ExitFailure, ExitSuccess))
 import System.Process (readProcessWithExitCode)
 import System.Timeout (timeout)
 import Tests (testcases)
 import Unshortener (genFile)
 
 tests :: IO [Test]
 tests = do
   let testDir = "test-tmp"
   setup testDir
   let testResults = map (createTest testDir) testcases
   pure testResults
 
 setup :: String -> IO ()
 setup = createDirectoryIfMissing False
 
 tearDown :: String -> IO ()
 tearDown = removeDirectoryRecursive
 
 createTest :: String -> (String, String) -> Test
 createTest topdir (testDir, f) =
   let test testDir f =
         TestInstance
           { run = Finished <$> performTest (topdir <> "/" <> testDir) f,
             name = f,
             tags = [],
             options = [],
             setOption = \_ _ -> Right $ test testDir f
           }
    in Test $ test testDir f
 
 performTest :: String -> String -> IO Result
 performTest testDir f = do
   createDirectoryIfMissing False testDir
-  copyFile "isabelle/SeCaV.thy" $ testDir <> "/SeCaV.thy"
+  copyFile "SeCaV.thy" $ testDir <> "/SeCaV.thy"
   copyFile "test/completeness/ROOT" $ testDir <> "/ROOT"
 
   let parse = sequentParser f
   case parse of
     Left e -> pure $ Fail $ show e
     Right fm -> do
       let (formula, names) = genInit fm
       let proofTree = secavProverCode formula
       let shortProof = initExtract names $ removeNoopRules $ extSurgery $ removeNoopRules $ expandMultiRules proofTree
       let proofParse = programParser shortProof
       case proofParse of
         Left e -> pure $ Fail $ show e
         Right proofAst -> do
           let isabelleProof = genFile "Test" proofAst
           writeFile (testDir <> "/Test.thy") isabelleProof
           (exit, _, error) <- readProcessWithExitCode "isabelle" ["build", "-D", testDir] []
           case exit of
             ExitFailure _ -> pure $ Fail error
             ExitSuccess -> pure Pass