diff --git a/thys/Gromov_Hyperbolicity/Eexp_Eln.thy b/thys/Gromov_Hyperbolicity/Eexp_Eln.thy index be2252bacd951cb0036762661c0797d811ebe69a_dGh5cy9Hcm9tb3ZfSHlwZXJib2xpY2l0eS9FZXhwX0Vsbi50aHk=..1282d34fd48c74fa27990d0b04a90e9c45afbc39_dGh5cy9Hcm9tb3ZfSHlwZXJib2xpY2l0eS9FZXhwX0Vsbi50aHk= 100644 --- a/thys/Gromov_Hyperbolicity/Eexp_Eln.thy +++ b/thys/Gromov_Hyperbolicity/Eexp_Eln.thy @@ -19,7 +19,7 @@ | "ennexp (\<infinity>) = \<infinity>" | "ennexp (-\<infinity>) = 0" by (auto intro: ereal_cases) -termination by standard (rule wf_empty) +termination by standard (rule wf_on_bot) lemma ennexp_0 [simp]: "ennexp 0 = 1" @@ -29,7 +29,7 @@ "eln (ennreal r) = (if r \<le> 0 then -\<infinity> else ereal (ln r))" | "eln (\<infinity>) = \<infinity>" by (auto intro: ennreal_cases, metis ennreal_eq_0_iff, simp add: ennreal_neg) -termination by standard (rule wf_empty) +termination by standard (rule wf_on_bot) lemma eln_simps [simp]: "eln 0 = -\<infinity>" diff --git a/thys/Gromov_Hyperbolicity/Gromov_Boundary.thy b/thys/Gromov_Hyperbolicity/Gromov_Boundary.thy index be2252bacd951cb0036762661c0797d811ebe69a_dGh5cy9Hcm9tb3ZfSHlwZXJib2xpY2l0eS9Hcm9tb3ZfQm91bmRhcnkudGh5..1282d34fd48c74fa27990d0b04a90e9c45afbc39_dGh5cy9Hcm9tb3ZfSHlwZXJib2xpY2l0eS9Hcm9tb3ZfQm91bmRhcnkudGh5 100644 --- a/thys/Gromov_Hyperbolicity/Gromov_Boundary.thy +++ b/thys/Gromov_Hyperbolicity/Gromov_Boundary.thy @@ -2701,7 +2701,7 @@ | "to_real_Gromov_completion (\<infinity>) = abs_Gromov_completion (\<lambda>n. n)" | "to_real_Gromov_completion (-\<infinity>) = abs_Gromov_completion (\<lambda>n. -n)" by (auto intro: ereal_cases) -termination by standard (rule wf_empty) +termination by standard (rule wf_on_bot) text \<open>To prove the bijectivity, we prove by hand injectivity and surjectivity using the above lemmas.\<close> diff --git a/thys/JinjaThreads/Compiler/Compiler1.thy b/thys/JinjaThreads/Compiler/Compiler1.thy index be2252bacd951cb0036762661c0797d811ebe69a_dGh5cy9KaW5qYVRocmVhZHMvQ29tcGlsZXIvQ29tcGlsZXIxLnRoeQ==..1282d34fd48c74fa27990d0b04a90e9c45afbc39_dGh5cy9KaW5qYVRocmVhZHMvQ29tcGlsZXIvQ29tcGlsZXIxLnRoeQ== 100644 --- a/thys/JinjaThreads/Compiler/Compiler1.thy +++ b/thys/JinjaThreads/Compiler/Compiler1.thy @@ -57,7 +57,7 @@ by pat_completeness auto termination apply(relation "case_sum (\<lambda>p. size (snd p)) (\<lambda>p. size_list size (snd p)) <*mlex*> {}") -apply(rule wf_mlex[OF wf_empty]) +apply(rule wf_mlex[OF wf_on_bot]) apply(rule mlex_less, simp)+ done diff --git a/thys/JinjaThreads/Compiler/TypeComp.thy b/thys/JinjaThreads/Compiler/TypeComp.thy index be2252bacd951cb0036762661c0797d811ebe69a_dGh5cy9KaW5qYVRocmVhZHMvQ29tcGlsZXIvVHlwZUNvbXAudGh5..1282d34fd48c74fa27990d0b04a90e9c45afbc39_dGh5cy9KaW5qYVRocmVhZHMvQ29tcGlsZXIvVHlwZUNvbXAudGh5 100644 --- a/thys/JinjaThreads/Compiler/TypeComp.thy +++ b/thys/JinjaThreads/Compiler/TypeComp.thy @@ -169,7 +169,7 @@ by pat_completeness simp_all termination apply(relation "case_sum (\<lambda>p. size (snd (snd (snd p)))) (\<lambda>p. size_list size (snd (snd (snd p)))) <*mlex*> {}") -apply(rule wf_mlex[OF wf_empty]) +apply(rule wf_mlex[OF wf_on_bot]) apply(rule mlex_less, simp)+ done diff --git a/thys/Signature_Groebner/Signature_Groebner.thy b/thys/Signature_Groebner/Signature_Groebner.thy index be2252bacd951cb0036762661c0797d811ebe69a_dGh5cy9TaWduYXR1cmVfR3JvZWJuZXIvU2lnbmF0dXJlX0dyb2VibmVyLnRoeQ==..1282d34fd48c74fa27990d0b04a90e9c45afbc39_dGh5cy9TaWduYXR1cmVfR3JvZWJuZXIvU2lnbmF0dXJlX0dyb2VibmVyLnRoeQ== 100644 --- a/thys/Signature_Groebner/Signature_Groebner.thy +++ b/thys/Signature_Groebner/Signature_Groebner.thy @@ -7511,7 +7511,7 @@ shows "rb_aux_dom args" proof - let ?rel = "rb_aux_term <*lex*> ({}::(nat \<times> nat) set)" - from wf_rb_aux_term wf_empty have "wf ?rel" .. + from wf_rb_aux_term wf_on_bot have "wf ?rel" .. thus ?thesis using assms proof (induct args) case (less args) diff --git a/thys/Skip_Lists/Skip_List.thy b/thys/Skip_Lists/Skip_List.thy index be2252bacd951cb0036762661c0797d811ebe69a_dGh5cy9Ta2lwX0xpc3RzL1NraXBfTGlzdC50aHk=..1282d34fd48c74fa27990d0b04a90e9c45afbc39_dGh5cy9Ta2lwX0xpc3RzL1NraXBfTGlzdC50aHk= 100644 --- a/thys/Skip_Lists/Skip_List.thy +++ b/thys/Skip_Lists/Skip_List.thy @@ -571,7 +571,7 @@ proof (relation "(\<lambda>(A,f,l,a,b). card A) <*mlex*> (\<lambda>(A,f,l,a,b). Max (f ` A) - l) <*mlex*> {}", goal_cases) case 1 then show ?case - by(intro wf_mlex wf_empty) + by(intro wf_mlex wf_on_bot) next case 2 then show ?case @@ -607,7 +607,7 @@ goal_cases) case 1 then show ?case - by(intro wf_mlex wf_empty) + by(intro wf_mlex wf_on_bot) next case 2 then show ?case