Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Extended_Real.thy
changeset 82299 a0693649e9c6
parent 81763 2cf8f8e4c1fd 
--- a/src/HOL/Library/Extended_Real.thy	Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Mon Mar 17 16:29:48 2025 +0100
@@ -298,7 +298,7 @@
 | "real_of_ereal \<infinity> = 0"
 | "real_of_ereal (-\<infinity>) = 0"
   by (auto intro: ereal_cases)
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
 
 lemma real_of_ereal[simp]:
   "real_of_ereal (- x :: ereal) = - (real_of_ereal x)"
@@ -327,7 +327,7 @@
 | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
 | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
 by (auto intro: ereal_cases)
-termination proof qed (rule wf_empty)
+termination proof qed (rule wf_on_bot)
 
 instance ..
 
@@ -377,7 +377,7 @@
   with prems show P
    by (cases rule: ereal2_cases[of a b]) auto
 qed auto
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
 
 lemma Infty_neq_0[simp]:
   "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -852,7 +852,7 @@
 | "sgn (\<infinity>::ereal) = 1"
 | "sgn (-\<infinity>::ereal) = -1"
 by (auto intro: ereal_cases)
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
 
 function times_ereal where
   "ereal r * ereal p = ereal (r * p)"
isabelle