diff --git a/thys/FOL_Seq_Calc3/Main.hs b/thys/FOL_Seq_Calc3/Main.hs
--- a/thys/FOL_Seq_Calc3/Main.hs
+++ b/thys/FOL_Seq_Calc3/Main.hs
@@ -1,59 +1,59 @@
 import Prelude
 import Data.Char (chr, ord)
 import Data.List (intersperse)
 import System.Environment
 
 import Arith
 import Prover
 
 instance Show Arith.Nat where
   show (Nat n) = show n
 
 charFrom :: Char -> Arith.Nat -> Char
 charFrom c n = chr (ord c + fromInteger (Arith.integer_of_nat n))
 
 instance Show Tm where
   show (Var n) = show n
   show (Fun f []) = charFrom 'a' f : ""
   show (Fun f ts) = charFrom 'f' f : "(" ++ concat (intersperse ", " (map show ts)) ++ ")"
 
 instance Show Fm where
-  show Falsity = "Falsity"
+  show Falsity = "Fls"
   show (Pre p []) = charFrom 'P' p : ""
   show (Pre p ts) = charFrom 'P' p : "(" ++ concat (intersperse ", " (map show ts)) ++ ")"
-  show (Imp p q) = "(" ++ show p ++ ") --> (" ++ show q ++ ")"
+  show (Imp p q) = "(" ++ show p ++ ") -> (" ++ show q ++ ")"
   show (Uni p) = "forall " ++ show p
 
 showRule :: Rule -> String
 showRule (Axiom n ts) = "Axiom on " ++ show (Pre n ts)
 showRule FlsL = "FlsL"
 showRule FlsR = "FlsR"
 showRule Idle = "Idle"
 showRule (ImpL p q) = "ImpL on " ++ show p ++ " and " ++ show q
 showRule (ImpR p q) = "ImpR on " ++ show p ++ " and " ++ show q
 showRule (UniL t p) = "UniL on " ++ show t ++ " and " ++ show p
 showRule (UniR p) = "UniR on " ++ show p
 
 showFms :: [Fm] -> String
 showFms ps = concat (intersperse ", " (map show ps))
 
 showTree :: Int -> Tree (([Fm], [Fm]), Rule) -> String
 showTree n (Node ((l, r), rule) (Abs_fset (Set ts))) =
   let inc = if length ts > 1 then 2 else 0 in
   replicate n ' ' ++ showFms l ++ " |- " ++ showFms r ++ "\n" ++
   replicate n ' ' ++ " + " ++ showRule rule ++ "\n" ++
   concat (map (showTree (n + inc)) ts)
 
 instance Read Arith.Nat where
   readsPrec d s = map (\(n, s) -> (Arith.Nat n, s)) (readsPrec d s :: [(Integer, String)])
 
 deriving instance Read Tm
 deriving instance Read Fm
 
 main :: IO ()
 main = do
   args <- getArgs
   let p = read (head args) :: Fm
   let res = prove p
   putStrLn (showTree 0 res)
 
diff --git a/thys/FOL_Seq_Calc3/Prover.thy b/thys/FOL_Seq_Calc3/Prover.thy
--- a/thys/FOL_Seq_Calc3/Prover.thy
+++ b/thys/FOL_Seq_Calc3/Prover.thy
@@ -1,48 +1,43 @@
 section \<open>Prover\<close>
 
 theory Prover imports "Abstract_Completeness.Abstract_Completeness" Encoding Fair_Stream begin
 
 function eff :: \<open>rule \<Rightarrow> sequent \<Rightarrow> (sequent fset) option\<close> where
-  \<open>eff Idle (A, B) =
-    Some {| (A, B) |}\<close>
-| \<open>eff (Axiom P ts) (A, B) = (if \<^bold>\<ddagger>P ts [\<in>] A \<and> \<^bold>\<ddagger>P ts [\<in>] B then
-    Some {||} else None)\<close>
-| \<open>eff FlsL (A, B) = (if \<^bold>\<bottom> [\<in>] A then
-    Some {||} else None)\<close>
-| \<open>eff FlsR (A, B) = (if \<^bold>\<bottom> [\<in>] B then
-    Some {| (A, B [\<div>] \<^bold>\<bottom>) |} else None)\<close>
+  \<open>eff Idle (A, B) = Some {| (A, B) |}\<close>
+| \<open>eff (Axiom P ts) (A, B) = (if \<^bold>\<ddagger>P ts [\<in>] A \<and> \<^bold>\<ddagger>P ts [\<in>] B then Some {||} else None)\<close>
+| \<open>eff FlsL (A, B) = (if \<^bold>\<bottom> [\<in>] A then Some {||} else None)\<close>
+| \<open>eff FlsR (A, B) = (if \<^bold>\<bottom> [\<in>] B then Some {| (A, B [\<div>] \<^bold>\<bottom>) |} else None)\<close>
 | \<open>eff (ImpL p q) (A, B) = (if (p \<^bold>\<longrightarrow> q) [\<in>] A then
     Some {| (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B), (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B) |} else None)\<close>
 | \<open>eff (ImpR p q) (A, B) = (if (p \<^bold>\<longrightarrow> q) [\<in>] B then
     Some {| (p # A, q # B [\<div>] (p \<^bold>\<longrightarrow> q)) |} else None)\<close>
-| \<open>eff (UniL t p) (A, B) = (if \<^bold>\<forall>p [\<in>] A then
-    Some {| (\<langle>t\<rangle>p # A, B) |} else None)\<close>
+| \<open>eff (UniL t p) (A, B) = (if \<^bold>\<forall>p [\<in>] A then Some {| (\<langle>t\<rangle>p # A, B) |} else None)\<close>
 | \<open>eff (UniR p) (A, B) = (if \<^bold>\<forall>p [\<in>] B then
     Some {| (A, \<langle>\<^bold>#(fresh (A @ B))\<rangle>p # B [\<div>] \<^bold>\<forall>p) |} else None)\<close>
   by pat_completeness auto
 termination by (relation \<open>measure size\<close>) standard
 
 definition rules :: \<open>rule stream\<close> where
   \<open>rules \<equiv> fair_stream rule_of_nat\<close>
 
 lemma UNIV_rules: \<open>sset rules = UNIV\<close>
   unfolding rules_def using UNIV_stream surj_rule_of_nat .
 
 interpretation RuleSystem \<open>\<lambda>r s ss. eff r s = Some ss\<close> rules UNIV
   by unfold_locales (auto simp: UNIV_rules intro: exI[of _ Idle])
 
 lemma per_rules':
   assumes \<open>enabled r (A, B)\<close> \<open>\<not> enabled r (A', B')\<close> \<open>eff r' (A, B) = Some ss'\<close> \<open>(A', B') |\<in>| ss'\<close>
   shows \<open>r' = r\<close>
   using assms by (cases r r' rule: rule.exhaust[case_product rule.exhaust])
     (unfold enabled_def, auto split: if_splits)
 
 lemma per_rules: \<open>per r\<close>
   unfolding per_def UNIV_rules using per_rules' by fast
 
 interpretation PersistentRuleSystem \<open>\<lambda>r s ss. eff r s = Some ss\<close> rules UNIV
   using per_rules by unfold_locales
 
 definition \<open>prover \<equiv> mkTree rules\<close>
 
 end
diff --git a/thys/FOL_Seq_Calc3/Syntax.thy b/thys/FOL_Seq_Calc3/Syntax.thy
--- a/thys/FOL_Seq_Calc3/Syntax.thy
+++ b/thys/FOL_Seq_Calc3/Syntax.thy
@@ -1,97 +1,90 @@
 section \<open>Syntax\<close>
 
 theory Syntax imports List_Syntax begin
 
 subsection \<open>Terms and Formulas\<close>
 
 datatype tm
   = Var nat (\<open>\<^bold>#\<close>)
   | Fun nat \<open>tm list\<close> (\<open>\<^bold>\<dagger>\<close>)
 
 datatype fm
   = Falsity (\<open>\<^bold>\<bottom>\<close>)
   | Pre nat \<open>tm list\<close> (\<open>\<^bold>\<ddagger>\<close>)
   | Imp fm fm (infixr \<open>\<^bold>\<longrightarrow>\<close> 55)
   | Uni fm (\<open>\<^bold>\<forall>\<close>)
 
 type_synonym sequent = \<open>fm list \<times> fm list\<close>
 
 subsubsection \<open>Substitution\<close>
 
 primrec add_env :: \<open>'a \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a\<close> (infix \<open>\<Zsemi>\<close> 0) where
   \<open>(t \<Zsemi> s) 0 = t\<close>
 | \<open>(t \<Zsemi> s) (Suc n) = s n\<close>
 
 primrec lift_tm :: \<open>tm \<Rightarrow> tm\<close> where
   \<open>lift_tm (\<^bold>#n) = \<^bold>#(n+1)\<close>
 | \<open>lift_tm (\<^bold>\<dagger>f ts) = \<^bold>\<dagger>f (map lift_tm ts)\<close>
 
 primrec sub_tm :: \<open>(nat \<Rightarrow> tm) \<Rightarrow> tm \<Rightarrow> tm\<close> where
   \<open>sub_tm s (\<^bold>#n) = s n\<close>
 | \<open>sub_tm s (\<^bold>\<dagger>f ts) = \<^bold>\<dagger>f (map (sub_tm s) ts)\<close>
 
 primrec sub_fm :: \<open>(nat \<Rightarrow> tm) \<Rightarrow> fm \<Rightarrow> fm\<close> where
-  \<open>sub_fm s \<^bold>\<bottom> = \<^bold>\<bottom>\<close>
+  \<open>sub_fm _ \<^bold>\<bottom> = \<^bold>\<bottom>\<close>
 | \<open>sub_fm s (\<^bold>\<ddagger>P ts) = \<^bold>\<ddagger>P (map (sub_tm s) ts)\<close>
 | \<open>sub_fm s (p \<^bold>\<longrightarrow> q) = sub_fm s p \<^bold>\<longrightarrow> sub_fm s q\<close>
 | \<open>sub_fm s (\<^bold>\<forall>p) = \<^bold>\<forall>(sub_fm (\<^bold>#0 \<Zsemi> \<lambda>n. lift_tm (s n)) p)\<close>
 
 abbreviation inst_single :: \<open>tm \<Rightarrow> fm \<Rightarrow> fm\<close> (\<open>\<langle>_\<rangle>\<close>) where
-  \<open>\<langle>t\<rangle>p \<equiv> sub_fm (t \<Zsemi> \<^bold>#) p\<close>
+  \<open>\<langle>t\<rangle> \<equiv> sub_fm (t \<Zsemi> \<^bold>#)\<close>
 
 subsubsection \<open>Variables\<close>
 
 primrec vars_tm :: \<open>tm \<Rightarrow> nat list\<close> where
   \<open>vars_tm (\<^bold>#n) = [n]\<close>
 | \<open>vars_tm (\<^bold>\<dagger>_ ts) = concat (map vars_tm ts)\<close>
 
 primrec vars_fm :: \<open>fm \<Rightarrow> nat list\<close> where
   \<open>vars_fm \<^bold>\<bottom> = []\<close>
 | \<open>vars_fm (\<^bold>\<ddagger>_ ts) = concat (map vars_tm ts)\<close>
 | \<open>vars_fm (p \<^bold>\<longrightarrow> q) = vars_fm p @ vars_fm q\<close>
 | \<open>vars_fm (\<^bold>\<forall>p) = vars_fm p\<close>
 
 primrec max_list :: \<open>nat list \<Rightarrow> nat\<close> where
   \<open>max_list [] = 0\<close>
 | \<open>max_list (x # xs) = max x (max_list xs)\<close>
 
 lemma max_list_append: \<open>max_list (xs @ ys) = max (max_list xs) (max_list ys)\<close>
   by (induct xs) auto
 
 lemma max_list_concat: \<open>xs [\<in>] xss \<Longrightarrow> max_list xs \<le> max_list (concat xss)\<close>
   by (induct xss) (auto simp: max_list_append)
 
 lemma max_list_in: \<open>max_list xs < n \<Longrightarrow> n [\<notin>] xs\<close>
   by (induct xs) auto
 
 definition vars_fms :: \<open>fm list \<Rightarrow> nat list\<close> where
   \<open>vars_fms A \<equiv> concat (map vars_fm A)\<close>
 
 lemma vars_fms_member: \<open>p [\<in>] A \<Longrightarrow> vars_fm p [\<subseteq>] vars_fms A\<close>
   unfolding vars_fms_def by (induct A) auto
 
 lemma max_list_mono: \<open>A [\<subseteq>] B \<Longrightarrow> max_list A \<le> max_list B\<close>
   by (induct A) (simp, metis linorder_not_le list.set_intros(1) max.absorb2 max.absorb3
       max_list.simps(2) max_list_in set_subset_Cons subset_code(1))
 
 lemma max_list_vars_fms:
   assumes \<open>max_list (vars_fms A) \<le> n\<close> \<open>p [\<in>] A\<close>
   shows \<open>max_list (vars_fm p) \<le> n\<close>
   using assms max_list_mono vars_fms_member by (meson dual_order.trans)
 
 definition fresh :: \<open>fm list \<Rightarrow> nat\<close> where
   \<open>fresh A \<equiv> Suc (max_list (vars_fms A))\<close>
 
 subsection \<open>Rules\<close>
 
-datatype rule
-  = Idle
-  | Axiom nat \<open>tm list\<close>
-  | FlsL
-  | FlsR
-  | ImpL fm fm
-  | ImpR fm fm
-  | UniL tm fm
-  | UniR fm
+datatype rule =
+  Idle | Axiom nat \<open>tm list\<close> | FlsL | FlsR | ImpL fm fm | ImpR fm fm | UniL tm fm | UniR fm
 
 end