# HG changeset patch
# User wenzelm
# Date 1661979556 -7200
# Node ID 39eae8f9dab4079b92c8cb1fc4860fb44c9d75c8
# Parent  5f94db3a7e2507771e1594bb3e4a81362b3ba087
eliminated tabs, assuming tab-width=8;

diff -r 5f94db3a7e25 -r 39eae8f9dab4 src/HOL/SMT_Examples/SMT_Examples_Verit.thy
--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy	Wed Aug 31 22:58:52 2022 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy	Wed Aug 31 22:59:16 2022 +0200
@@ -753,36 +753,36 @@
 https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20smt.20.28verit.29.3A.20exception.20THM.200.20raised.20.28line.20312.20.2E.2E.2E/near/290088165
 *)
 lemma "\<lbrakk>\<forall>x y. (\<forall>xa s. is_fail (run (x xa) s) \<or>
-		   is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
-		   (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
+                   is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
+                   (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
 \<longrightarrow>
-	   (\<forall>s. is_fail (run (B x) s) \<or>
-		is_fail (run (B y) s) = is_fail (run (B x) s) \<and>
-		(\<forall>a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
+           (\<forall>s. is_fail (run (B x) s) \<or>
+                is_fail (run (B y) s) = is_fail (run (B x) s) \<and>
+                (\<forall>a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
      \<And>y. \<forall>x ya. (\<forall>xa s. is_fail (run (x xa) s) \<or>
-			 is_fail (run (ya xa) s) = is_fail (run (x xa) s) \<and>
-			 (\<forall>a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
+                         is_fail (run (ya xa) s) = is_fail (run (x xa) s) \<and>
+                         (\<forall>a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
 \<longrightarrow>
-		 (\<forall>s. is_fail (run (C y x) s) \<or>
-		      is_fail (run (C y ya) s) = is_fail (run (C y x) s) \<and>
-		      (\<forall>a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a,
+                 (\<forall>s. is_fail (run (C y x) s) \<or>
+                      is_fail (run (C y ya) s) = is_fail (run (C y x) s) \<and>
+                      (\<forall>a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a,
 b)))\<rbrakk>
     \<Longrightarrow> \<forall>x y. (\<forall>xa s.
-		  is_fail (run (x xa) s) \<or>
-		  is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
-		  (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
+                  is_fail (run (x xa) s) \<or>
+                  is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
+                  (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
 \<longrightarrow>
-	      (\<forall>s. is_fail (run (B x) s) \<or>
-		   (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b)) \<or>
-		   (is_fail (run (B y) s) \<or> (\<exists>a b. is_res (run (B y) s) (a, b) \<and>
+              (\<forall>s. is_fail (run (B x) s) \<or>
+                   (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b)) \<or>
+                   (is_fail (run (B y) s) \<or> (\<exists>a b. is_res (run (B y) s) (a, b) \<and>
 is_fail (run (C a y) b))) =
-		   (is_fail (run (B x) s) \<or> (\<exists>a b. is_res (run (B x) s) (a, b) \<and>
+                   (is_fail (run (B x) s) \<or> (\<exists>a b. is_res (run (B x) s) (a, b) \<and>
 is_fail (run (C a x) b))) \<and>
-		   (\<forall>a b. (is_fail (run (B y) s) \<or>
-			   (\<exists>aa ba. is_res (run (B y) s) (aa, ba) \<and> is_res (run (C aa y)
+                   (\<forall>a b. (is_fail (run (B y) s) \<or>
+                           (\<exists>aa ba. is_res (run (B y) s) (aa, ba) \<and> is_res (run (C aa y)
 ba) (a, b))) =
-			  (is_fail (run (B x) s) \<or>
-			   (\<exists>aa ba. is_res (run (B x) s) (aa, ba) \<and> is_res (run (C aa x)
+                          (is_fail (run (B x) s) \<or>
+                           (\<exists>aa ba. is_res (run (B x) s) (aa, ba) \<and> is_res (run (C aa x)
 ba) (a, b)))))"  
   apply (rule duplicate_goal)
   subgoal