Fix usage of fresh_cases theorem

jvanbruegge · Nov 21, 2024 · a479bcd · a479bcd
1 parent 2f9551b
commit a479bcd
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git a/thys/Infinitary_Lambda_Calculus/ILC.thy b/thys/Infinitary_Lambda_Calculus/ILC.thy
@@ -358,7 +358,7 @@ lemma iLam_avoid: "|A::ivar set| <o |UNIV::ivar set| \<Longrightarrow> \<exists>
    apply (rule trans)
     apply (rule sym)
     apply assumption
-  apply (rotate_tac 2)
+  apply (rotate_tac 3)
    apply assumption
   apply (drule iffD1[OF disjoint_iff])
   by auto

diff --git a/thys/Pi_Calculus/Commitment.thy b/thys/Pi_Calculus/Commitment.thy
@@ -364,7 +364,7 @@ local_setup \<open>MRBNF_Sugar.register_binder_sugar "Commitment.commit" {
     SOME @{term "\<lambda>x P. bns x"}
   ]],
   bset_bounds = @{thms bns_bound},
-  strong_induct = @{thm refl},
+  strong_induct = NONE,
   mrbnf = the (MRBNF_Def.mrbnf_of @{context} "Commitment.commit_pre"),
   set_simpss = [],
   subst_simps = NONE

diff --git a/thys/Pi_Calculus/Pi.thy b/thys/Pi_Calculus/Pi.thy
@@ -226,7 +226,7 @@ lemma Abs_avoid: "|A::var set| <o |UNIV::var set| \<Longrightarrow> \<exists>x'
    apply (rule trans)
     apply (rule sym)
     apply assumption
-  apply (rotate_tac 2)
+  apply (rotate_tac 3)
    apply assumption
   apply (drule iffD1[OF disjoint_iff])
   apply (erule allE)

diff --git a/thys/STLC/STLC.thy b/thys/STLC/STLC.thy
@@ -174,7 +174,7 @@ lemma Abs_avoid: "|A::'a::var_terms_pre set| <o |UNIV::'a set| \<Longrightarrow>
    apply (rule trans)
     apply (rule sym)
     apply assumption
-  apply (rotate_tac 2)
+  apply (rotate_tac 3)
    apply assumption
   apply (drule iffD1[OF disjoint_iff])
   apply (erule allE)

diff --git a/thys/Untyped_Lambda_Calculus/LC.thy b/thys/Untyped_Lambda_Calculus/LC.thy
@@ -253,7 +253,7 @@ lemma Lam_avoid: "|A::var set| <o |UNIV::var set| \<Longrightarrow> \<exists>x'
    apply (rule trans)
     apply (rule sym)
     apply assumption
-  apply (rotate_tac 2)
+  apply (rotate_tac 3)
    apply assumption
   apply (drule iffD1[OF disjoint_iff])
   apply (erule allE)