diekmann · jsoref · Oct 22, 2021 · Oct 22, 2021 · Oct 22, 2021 · Oct 22, 2021
diff --git a/README.md b/README.md
@@ -54,7 +54,7 @@ See README.md in [haskell_tool](./haskell_tool/).
   * Cornelius Diekmann, Lukas Schwaighofer, and Georg Carle. *Certifying spoofing-protection of firewalls.* In 11th International Conference on Network and Service Management, CNSM, Barcelona, Spain, November 2015. [[preprint]](http://www.net.in.tum.de/fileadmin/bibtex/publications/papers/diekmann2015_cnsm.pdf), [[ieee | paywall]](http://ieeexplore.ieee.org/document/7367354/)
   * Cornelius Diekmann, Lars Hupel, and Georg Carle. *Semantics-Preserving Simplification of Real-World Firewall Rule Sets.* In 20th International Symposium on Formal Methods, June 2015. [[preprint]](http://www.net.in.tum.de/fileadmin/bibtex/publications/papers/fm15_Semantics-Preserving_Simplification_of_Real-World_Firewall_Rule_Sets.pdf), [[springer | paywall]](http://link.springer.com/chapter/10.1007%2F978-3-319-19249-9_13)
 
-The raw data of the iptables rulesets from the Examples is stored in [this](https://github.com/diekmann/net-network) repositoy.
+The raw data of the iptables rulesets from the Examples is stored in [this](https://github.com/diekmann/net-network) repository.
 
 ---
 

diff --git a/haskell_tool/README.md b/haskell_tool/README.md
@@ -57,7 +57,7 @@ Available options:
   --routingtbl STRING      Optional path to a routing table.
   --table STRING           The table to load for analysis. Default: `filter`.
                            Note: This tool does not support packet modification,
-                           so loading tables such as `nat` will most likeley
+                           so loading tables such as `nat` will most likely
                            fail.
   --chain STRING           The chain to start the analysis. Default: `FORWARD`.
                            Use `INPUT` for a host-based firewall.

diff --git a/haskell_tool/lib/Data_Bits.README b/haskell_tool/lib/Data_Bits.README
@@ -1,3 +1,3 @@
-Automaticalyy generated by AFP Native_Word entry!!
+Automatically generated by AFP Native_Word entry!!
 Do not edit!
 Regenerate each time!
diff --git a/haskell_tool/lib/Network/IPTables/Analysis.hs b/haskell_tool/lib/Network/IPTables/Analysis.hs
@@ -58,7 +58,7 @@ certifySpoofingProtection_generic
         (IsabelleIpAssmt a -> [Isabelle.Rule (Isabelle.Common_primitive a)] -> [String])
          -> IsabelleIpAssmt a -> [Isabelle.Rule (Isabelle.Common_primitive a)] -> ([String], [(Isabelle.Iface, Bool)])
 certifySpoofingProtection_generic debug_ipassmt_f ipassmt rs = (warn_defined ++ debug_ipassmt, certResult)
-    where -- fuc: firewall under certification, prepocessed
+    where -- fuc: firewall under certification, preprocessed
           -- no_spoofing_executable_set requires normalized_nnf_match. Isabelle.upper_closure guarantees this.
           -- It also guarantees that if we start from a simple_ruleset, it remains a simple ruleset.
           -- Theorem: no_spoofing_executable_set_preprocessed

diff --git a/haskell_tool/lib/Network/IPTables/Main.hs b/haskell_tool/lib/Network/IPTables/Main.hs
@@ -45,7 +45,7 @@ data CommandLineArgsLabeled = CommandLineArgsLabeled
         { verbose :: Bool <?> "Show verbose debug output (for example, of the parser)."
         , ipassmt :: Maybe FilePath  <?> "Optional path to an IP assignment file. If not specified, it only loads `lo = [127.0.0.0/8]`."
         , routingtbl :: Maybe FilePath  <?> "Optional path to a routing table."
-        , table :: Maybe String <?> "The table to load for analysis. Default: `filter`. Note: This tool does not support packet modification, so loading tables such as `nat` will most likeley fail."
+        , table :: Maybe String <?> "The table to load for analysis. Default: `filter`. Note: This tool does not support packet modification, so loading tables such as `nat` will most likely fail."
         , chain :: Maybe String <?> "The chain to start the analysis. Default: `FORWARD`. Use `INPUT` for a host-based firewall."
         --TODO: we need some grouping for specific options for the analysis
         -- For example ./fffuu --analysis service-matrix --sport 424242 --analysis spoofing --foo
@@ -56,7 +56,7 @@ data CommandLineArgsLabeled = CommandLineArgsLabeled
 instance ParseRecord CommandLineArgsLabeled
 
 
--- unlabeld, mandatory command line arguments. For example: ./fffuu "path/to/iptables-save"
+-- unlabeled, mandatory command line arguments. For example: ./fffuu "path/to/iptables-save"
 -- http://stackoverflow.com/questions/36375556/haskell-unnamed-command-line-arguments-for-optparse-generic/36382477#36382477
 data CommandLineArgsUnlabeled = CommandLineArgsUnlabeled
         (FilePath <?> "Required: Path to `iptables-save` output. This is the input for this tool.")
@@ -133,7 +133,7 @@ main' ops = do
                     \It abstracts over unknown matches. \
                     \By default, it does an overapproximation, i.e. it loads a more permissive version of the ruleset. \
                     \Then it runs a number of analysis. \
-                    \Overapproximation means: if the anaylsis concludes that the packets you want to be dropped are dropped in the loaded overapproximation, then they are also dropped for your real firewall (without approximation)."
+                    \Overapproximation means: if the analysis concludes that the packets you want to be dropped are dropped in the loaded overapproximation, then they are also dropped for your real firewall (without approximation)."
     --print (cmdArgs::CommandLineArgs)
     (verbose, ipassmt, rtbl, table, chain, smOptions, (srcname, src)) <- readArgs ops cmdArgs
 

diff --git a/haskell_tool/lib/Network/IPTables/Ruleset.hs b/haskell_tool/lib/Network/IPTables/Ruleset.hs
@@ -156,7 +156,7 @@ filter_Isabelle_Action ps = case fAction ps of [] -> Isabelle.Empty
 
 
 
--- this is just DEBUGING
+-- this is just DEBUGGING
 -- tries to catch errors of rulesetLookup
 checkParsedTables :: Isabelle.Len a => Ruleset a -> IO ()
 checkParsedTables res = mapM_ check tables
@@ -168,7 +168,7 @@ checkParsedTables res = mapM_ check tables
           errormsg t msg = concat ["Table `", t ,"' caught exception: `"
                                    , msg
                                    , "'. Analysis not possible for this table. "
-                                   , "This is probably due to unsupportd actions "
+                                   , "This is probably due to unsupported actions "
                                    , "(or a bug in the parser)."]
           success t chain = concat ["Parsed ", show (length chain)
                                    , " chains in table ", t, ", a total of "

diff --git a/haskell_tool/test/Suites/GoldenFiles/help b/haskell_tool/test/Suites/GoldenFiles/help
@@ -4,7 +4,7 @@ and loads one table and chain. By default, it loads the `filter` table and the
 where only `ACCEPT` and `DROP` actions remain. It abstracts over unknown
 matches. By default, it does an overapproximation, i.e. it loads a more
 permissive version of the ruleset. Then it runs a number of analysis.
-Overapproximation means: if the anaylsis concludes that the packets you want to
+Overapproximation means: if the analysis concludes that the packets you want to
 be dropped are dropped in the loaded overapproximation, then they are also
 dropped for your real firewall (without approximation).
 
@@ -21,7 +21,7 @@ Available options:
   --routingtbl STRING      Optional path to a routing table.
   --table STRING           The table to load for analysis. Default: `filter`.
                            Note: This tool does not support packet modification,
-                           so loading tables such as `nat` will most likeley
+                           so loading tables such as `nat` will most likely
                            fail.
   --chain STRING           The chain to start the analysis. Default: `FORWARD`.
                            Use `INPUT` for a host-based firewall.

diff --git a/haskell_tool/test/Suites/GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating b/haskell_tool/test/Suites/GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating
@@ -2,8 +2,8 @@ Parsed IpAssmt
 IpAssmt [(eth0,Pos [0.0.0.0-255.255.255.255]),(foo,Pos []),(eth1.96,Pos [131.159.14.3/25]),(eth1.108,Pos [131.159.14.129/26]),(eth1.109,Pos [131.159.20.11/24]),(eth1.110,Neg [131.159.14.0/23,131.159.20.0/23,192.168.212.0/23,188.95.233.0/24,188.95.232.192/27,188.95.234.0/23,192.48.107.0/24,188.95.236.0/22,185.86.232.0/22]),(eth1.116,Pos [131.159.15.131/26]),(eth1.152,Pos [131.159.15.252/28]),(eth1.171,Pos [131.159.15.2/26]),(eth1.173,Pos [131.159.21.252/24]),(eth1.1010,Pos [131.159.15.227/28]),(eth1.1011,Pos [131.159.14.194/27]),(eth1.1012,Pos [131.159.14.238/28]),(eth1.1014,Pos [131.159.15.217/27]),(eth1.1016,Pos [131.159.15.66/26]),(eth1.1017,Pos [131.159.14.242/28]),(eth1.1111,Pos [192.168.212.4/24]),(eth1.97,Pos [188.95.233.2/24]),(eth1.1019,Pos [188.95.234.2/23]),(eth1.1020,Pos [192.48.107.2/24]),(eth1.1023,Pos [188.95.236.2/22]),(eth1.1025,Pos [185.86.232.2/22]),(eth1.1024,Neg [131.159.14.0/23,131.159.20.0/23,192.168.212.0/23,188.95.233.0/24,188.95.232.192/27,188.95.234.0/23,192.48.107.0/24,188.95.236.0/22,185.86.232.0/22])]
 == Checking which tables are supported for analysis. Usually, only `filter'. ==
 Parsed 90 chains in table filter, a total of 4813 rules
-Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser).
-Table `raw' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser).
+Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser).
+Table `raw' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser).
 == Transformed to Isabelle type (only filter table) ==
 == unfolded FORWARD chain (upper closure) ==
 (-m state --state ESTABLISHED,RELATED,UNTRACKED, -j ACCEPT)

diff --git a/haskell_tool/test/Suites/GoldenFiles/sqrl_2015_aug_iptables-save-spoofing-protection b/haskell_tool/test/Suites/GoldenFiles/sqrl_2015_aug_iptables-save-spoofing-protection
@@ -134,8 +134,8 @@ INFO: Officially, we only support the filter table. You requested the `raw' tabl
 INFO: Officially, we only support the chains FORWARD, INPUT, OUTPUT. You requested the `PREROUTING' chain. Let's see what happens ;-)
 == Checking which tables are supported for analysis. Usually, only `filter'. ==
 Parsed 7 chains in table filter, a total of 53 rules
-Table `mangle' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser).
-Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser).
+Table `mangle' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser).
+Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser).
 Parsed 3 chains in table raw, a total of 12 rules
 == Transformed to Isabelle type (only raw table) ==
 [("OUTPUT",[]),("PREROUTING",[(-i lup, -j lupSpoofProtect (call)),(! -s 10.13.42.136/29 -i ldit, -j DROP),(! -s 10.13.42.128/29 -i lmd, -j DROP),(! -s 10.13.42.144/28 -i loben, -j DROP),(! -s 10.13.42.176/28 -i wg, -j DROP),(! -s 10.13.42.160/28 -i wt, -j DROP)]),("lupSpoofProtect",[(-s 192.168.0.0/16, -j DROP),(-s 10.0.0.0/8, -j DROP),(-s 172.16.0.0/12, -j DROP),(-d 192.168.0.0/16, -j DROP),(-d 10.0.0.0/8, -j DROP),(-d 172.16.0.0/12, -j DROP)])]

diff --git a/haskell_tool/test/Suites/Parser.hs b/haskell_tool/test/Suites/Parser.hs
@@ -10,7 +10,7 @@ import Test.Tasty
 import Test.Tasty.HUnit as HU
 
 
--- we always have "-m protocolid:0" (note the 0) because we havn't filled the protocol yet
+-- we always have "-m protocolid:0" (note the 0) because we haven't filled the protocol yet
 expected_result = "*filter\n\
     \:DOS~Pro-t_ect - [0:0]\n\
     \:FORWARD DROP [0:0]\n\
@@ -323,7 +323,7 @@ test_service_matrix ipassmtMaybeString fileName expected_result errormsg = do
 
 
 test_topoS_generated_service_matrix = HU.testCase "test_topoS_generated_service_matrix" $ test_service_matrix Nothing rulesetFile expected_result errormsg
-    where rulesetFile = "../thy/Iptables_Semantics/Examples/topoS_generated/imaginray_factory_network.iptables-save.by-linux-kernel"
+    where rulesetFile = "../thy/Iptables_Semantics/Examples/topoS_generated/imaginary_factory_network.iptables-save.by-linux-kernel"
           errormsg = "service marix topoS_generated differs"
           expected_result = ([
               ("10.8.8.1","10.8.8.1")

diff --git a/haskell_tool/test/Suites/ParserHelper.hs b/haskell_tool/test/Suites/ParserHelper.hs
@@ -13,7 +13,7 @@ import Test.Tasty.HUnit as HU
 
 
 
-test_parse_show_identiy parser str = HU.testCase ("ParserHelper: parse show identity ("++str++")") $ do
+test_parse_show_identity parser str = HU.testCase ("ParserHelper: parse show identity ("++str++")") $ do
     let result = case runParser eofParser () "<test data>" str
                 of Left err -> do error $ show err
                    Right result -> show result
@@ -36,21 +36,21 @@ test_parse_quotedstring str = HU.testCase ("ParserHelper: quoted string (`"++str
 --TODO negative tests!
 
 tests = testGroup "ParserHelper Unit tests" $
-  [ test_parse_show_identiy Network.IPTables.ParserHelper.ipv4addr "192.168.0.1"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv4cidr "192.168.0.1/24"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv4range "192.168.0.1-192.168.0.255"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6cidr "::/64"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6range "::-::"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "2001:db8::8:800:200c:417a"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "ff01::101"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::8:800:200c:417a"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "2001:db8::"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "ff00::"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "fe80::"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::1"
-  , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "2001:db8::1"
+  [ test_parse_show_identity Network.IPTables.ParserHelper.ipv4addr "192.168.0.1"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv4cidr "192.168.0.1/24"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv4range "192.168.0.1-192.168.0.255"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6cidr "::/64"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6range "::-::"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "2001:db8::8:800:200c:417a"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "ff01::101"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::8:800:200c:417a"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "2001:db8::"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "ff00::"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "fe80::"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::1"
+  , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "2001:db8::1"
   , test_parse_quotedstring "\"foo\""
   , test_parse_quotedstring "\"foo with some \\\" escaped quote \""
   , test_parse_quotedstring "\"foo with some escaped escape (\\\\) and proper ending quote \\\\\""

diff --git a/thy/Automatic_Refinement/Autoref_Bindings_HOL.thy b/thy/Automatic_Refinement/Autoref_Bindings_HOL.thy
@@ -611,7 +611,7 @@ subsection "Examples"
 
 text {* Be careful to make the concrete type a schematic type variable.
   The default behaviour of @{text "schematic_lemma"} makes it a fixed variable,
-  that will not unify with the infered term! *}
+  that will not unify with the inferred term! *}
 schematic_goal 
   "(?f::?'c,[1,2,3]@[4::nat])\<in>?R"
   by autoref

diff --git a/thy/Automatic_Refinement/Lib/Foldi.thy b/thy/Automatic_Refinement/Lib/Foldi.thy
@@ -1,7 +1,7 @@
-(*  Title:       Interuptible Fold
+(*  Title:       Interruptible Fold
     Author:      Thomas Tuerk <tuerk@in.tum.de>
 *)
-section {* Interuptible Fold *}
+section {* Interruptible Fold *}
 theory Foldi
 imports Main 
 begin

diff --git a/thy/Automatic_Refinement/Lib/Misc.thy b/thy/Automatic_Refinement/Lib/Misc.thy
@@ -6,7 +6,7 @@
 
 (*
   CHANGELOG:
-    2010-05-09: Removed AC, AI locales, they are superseeded by concepts
+    2010-05-09: Removed AC, AI locales, they are superseded by concepts
                   from OrderedGroups
     2010-09-22: Merges with ext/Aux
 

diff --git a/thy/Automatic_Refinement/Lib/Refine_Util.thy b/thy/Automatic_Refinement/Lib/Refine_Util.thy
@@ -637,7 +637,7 @@ ML {*
         "resolve with premises"
       #> Method.setup @{binding elim_all}
          (Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (elim_all_tac ctxt thms)))
-         "repeteadly apply elimination rules to all subgoals"
+         "repeatedly apply elimination rules to all subgoals"
       #> Method.setup @{binding subst_tac} eqsubst_inst_meth
          "single-step substitution (dynamic instantiation)"
       #> Method.setup @{binding clarsimp_all} (

diff --git a/thy/Automatic_Refinement/Parametricity/Param_Tool.thy b/thy/Automatic_Refinement/Parametricity/Param_Tool.thy
@@ -305,7 +305,7 @@ begin
   subsection \<open>Convenience Tools\<close>
 
   ML {*
-    (* Prefix p_ or wrong type supresses generation of relAPP *)
+    (* Prefix p_ or wrong type suppresses generation of relAPP *)
 
     fun cnv_relAPP t = let
       fun consider (Var ((name,_),T)) =

diff --git a/thy/Automatic_Refinement/Parametricity/Relators.thy b/thy/Automatic_Refinement/Parametricity/Relators.thy
@@ -758,7 +758,7 @@ lemma sv_add_invar:
 
 
 
-subsection {* Miscellanneous *}
+subsection {* Miscellaneous *}
 lemma rel_cong: "(f,g)\<in>Id \<Longrightarrow> (x,y)\<in>Id \<Longrightarrow> (f x, g y)\<in>Id" by simp
 lemma rel_fun_cong: "(f,g)\<in>Id \<Longrightarrow> (f x, g x)\<in>Id" by simp
 lemma rel_arg_cong: "(x,y)\<in>Id \<Longrightarrow> (f x, f y)\<in>Id" by simp

diff --git a/thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy b/thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy
@@ -10,7 +10,7 @@ text {*
   Priority tags are used to influence the ordering of refinement theorems.
   A priority tag defines two numeric priorities, a major and a minor priority.
   The major priority is considered first, the minor priority last, i.e., after
-  the homogenity and relator-priority criteria.
+  the homogeneity and relator-priority criteria.
   The default value for both priorities is 0.
 *}
 definition PRIO_TAG :: "int \<Rightarrow> int \<Rightarrow> bool" 
@@ -459,12 +459,12 @@ ML {*
 
     structure hom_rules = Named_Sorted_Thms (
       val name = @{binding autoref_hom}
-      val description = "Autoref: Homogenity rules"
+      val description = "Autoref: Homogeneity rules"
       val sort = K I
       val transform = K (
         fn thm => case Thm.concl_of thm of 
           @{mpat "Trueprop (CONSTRAINT _ _)"} => [thm]
-        | _ => raise THM ("Invalid homogenity rule",~1,[thm])
+        | _ => raise THM ("Invalid homogeneity rule",~1,[thm])
       )
     )
 

diff --git a/thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy b/thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy
@@ -4,7 +4,7 @@ imports Autoref_Translate
 begin
 
 (* TODO/FIXME: The priority ordering is not yet suited for generic
-  algorithms! If a refinement rule is generic, the homogenity and relator
+  algorithms! If a refinement rule is generic, the homogeneity and relator
   measures make no sense, as they are applied to schematic variables.
   However, currently generic algorithms seem to have lower priority than
   specific ones, so we can probably live with this problem for a while.

diff --git a/thy/Automatic_Refinement/Tool/Autoref_Tool.thy b/thy/Automatic_Refinement/Tool/Autoref_Tool.thy
@@ -107,13 +107,13 @@ method_setup autoref_trans_step = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (
     Autoref_Translate.trans_dbg_step_tac (Autoref_Phases.init_data ctxt)
   ))
-  *} "Single translation step, leaving unsolved side-coditions"
+  *} "Single translation step, leaving unsolved side-conditions"
 
 method_setup autoref_trans_step_only = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (
     Autoref_Translate.trans_step_only_tac (Autoref_Phases.init_data ctxt)
   ))
-  *} "Single translation step, not attempting to solve side-coditions"
+  *} "Single translation step, not attempting to solve side-conditions"
 
 method_setup autoref_side = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (

diff --git a/thy/Automatic_Refinement/Tool/Autoref_Translate.thy b/thy/Automatic_Refinement/Tool/Autoref_Translate.thy
@@ -269,7 +269,7 @@ ML {*
 
         val msg = case concl of
           @{mpat "Trueprop (DEFER_tag _)"} 
-            => Pretty.str "Could not solve defered side condition"
+            => Pretty.str "Could not solve deferred side condition"
         | @{mpat "Trueprop ((_,_)\<in>_)"} 
             => Pretty.str "Could not refine subterm"
         | _ => Pretty.str "Internal: Unexpected goal"